MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaodan Structured version   Visualization version   GIF version

Theorem jaodan 825
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
jaodan.1 ((𝜑𝜓) → 𝜒)
jaodan.2 ((𝜑𝜃) → 𝜒)
Assertion
Ref Expression
jaodan ((𝜑 ∧ (𝜓𝜃)) → 𝜒)

Proof of Theorem jaodan
StepHypRef Expression
1 jaodan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 450 . . 3 (𝜑 → (𝜓𝜒))
3 jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 450 . . 3 (𝜑 → (𝜃𝜒))
52, 4jaod 395 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 445 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386
This theorem is referenced by:  mpjaodan  826  andi  910  ccase  986  mpjao3dan  1392  relop  5242  poltletr  5497  ordnbtwn  5785  oeoa  7637  oeoe  7639  phplem3  8101  ssnnfi  8139  unwdomg  8449  numwdom  8842  infpssrlem5  9089  fin23lem24  9104  fin23lem28  9122  fin1a2lem10  9191  zornn0g  9287  gchdomtri  9411  fpwwe2lem12  9423  fpwwe2lem13  9424  msqgt0  10508  recextlem2  10618  lemul1a  10837  nnnn0addcl  11283  un0addcl  11286  un0mulcl  11287  elz2  11354  mul2lt0bi  11896  xaddnemnf  12026  xaddnepnf  12027  rexmul  12060  xlemul1a  12077  xrsupsslem  12096  xrinfmsslem  12097  ixxun  12149  fzsplit2  12324  fzsuc2  12356  elfzp12  12376  seqf1olem2  12797  expp1  12823  expneg  12824  expcllem  12827  mulexpz  12856  expaddz  12860  expmulz  12862  faclbnd4lem3  13038  faclbnd4lem4  13039  faclbnd4  13040  bcpasc  13064  ccatass  13326  ccatrn  13327  ccatswrd  13410  cats1un  13429  revccat  13468  summo  14397  sumss2  14406  fsumsplit  14420  geomulcvg  14551  fprodsplit  14640  bpoly2  14732  bpoly3  14733  ef0lem  14753  odd2np1  15008  sadcaddlem  15122  gcdcllem3  15166  dvdslcm  15254  lcmeq0  15256  lcmcl  15257  lcmneg  15259  lcmgcd  15263  rpexp1i  15376  pcid  15520  4sqlem16  15607  funcres2c  16501  lubun  17063  mulgneg  17500  mulgnn0z  17507  frgpup3lem  18130  gsumzunsnd  18295  gsumunsnfd  18296  dprddisj2  18378  dmdprdsplit2  18385  dprdsplit  18387  gsumdixp  18549  lssvs0or  19050  evlslem4  19448  refun0  21258  txhaus  21390  xkoptsub  21397  ptunhmeo  21551  xpsxmetlem  22124  xpsmet  22127  mbfss  23353  itg1addlem2  23404  iblss2  23512  itgsplit  23542  limcres  23590  ftc1lem5  23741  coe1mul3  23797  dgrlt  23960  abelthlem3  24125  atanlogaddlem  24574  atanlogsub  24577  atans2  24592  efrlim  24630  bposlem2  24944  lgsdir2lem4  24987  2sqb  25091  pntpbnd1  25209  ostthlem1  25250  hlbtwn  25440  cgracol  25653  inaghl  25665  brbtwn2  25719  axcontlem2  25779  isoun  29363  nn0sqeq1  29397  eliccelico  29424  elicoelioo  29425  fzsplit3  29436  xrge0iifhom  29807  esumsplit  29938  esumpad2  29941  sibfinima  30224  bnj1137  30824  subfacp1lem4  30926  subfacp1lem5  30927  mclsax  31227  nosepdm  31621  poimirlem2  33082  poimirlem8  33088  poimirlem22  33102  poimirlem28  33108  ftc1cnnc  33155  ftc1anclem2  33157  eqfnun  33187  fdc  33212  incsequz2  33216  unichnidl  33501  lkrss2N  33975  cdlemg27b  35503  tendoex  35782  dihmeetlem2N  36107  dvh3dim3N  36257  rexzrexnn0  36887  pell14qrexpcl  36950  elpell1qr2  36955  acongeq  37069  jm2.23  37082  rpnnen3  37118  radcnvrat  38034  sumpair  38716  cncfiooicclem1  39441  fourierdlem80  39740  fourierdlem93  39753  ccatpfx  40738
  Copyright terms: Public domain W3C validator