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

Theorem jaod 394
 Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)
Hypotheses
Ref Expression
jaod.1 (𝜑 → (𝜓𝜒))
jaod.2 (𝜑 → (𝜃𝜒))
Assertion
Ref Expression
jaod (𝜑 → ((𝜓𝜃) → 𝜒))

Proof of Theorem jaod
StepHypRef Expression
1 jaod.1 . . . 4 (𝜑 → (𝜓𝜒))
21com12 32 . . 3 (𝜓 → (𝜑𝜒))
3 jaod.2 . . . 4 (𝜑 → (𝜃𝜒))
43com12 32 . . 3 (𝜃 → (𝜑𝜒))
52, 4jaoi 393 . 2 ((𝜓𝜃) → (𝜑𝜒))
65com12 32 1 (𝜑 → ((𝜓𝜃) → 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382 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 384 This theorem is referenced by:  mpjaod  395  orel2  397  pm2.621  423  jaao  532  jaodan  861  pm2.63  864  ecase2d  1018  ecase3d  1021  dedlema  1032  dedlemb  1033  cad0  1705  psssstr  3855  eqoreldif  4369  opthpr  4528  prel12g  4544  opthprneg  4545  sotric  5213  sotr2  5216  relop  5428  suctr  5969  trsucss  5972  ordelinel  5986  ordelinelOLD  5987  fununi  6125  fnprb  6636  soisoi  6741  ordunisuc2  7209  poxp  7457  soxp  7458  wfrlem14  7597  wfrlem15  7598  tfrlem11  7653  omordi  7815  om00  7824  odi  7828  omeulem2  7832  oewordi  7840  nnmordi  7880  omsmolem  7902  swoord2  7943  nneneq  8308  dffi3  8502  inf3lem6  8703  cantnfle  8741  cantnflem1  8759  cantnflem2  8760  r1sdom  8810  r1ord3g  8815  rankxplim3  8917  carddom2  8993  wdomnumr  9077  alephordi  9087  alephdom  9094  cardaleph  9102  cdainf  9206  cfsuc  9271  cfsmolem  9284  sornom  9291  fin23lem25  9338  fin1a2lem11  9424  fin1a2s  9428  zorn2lem7  9516  ttukeylem5  9527  alephval2  9586  fpwwe2lem13  9656  gch2  9689  gchaclem  9692  prub  10008  sqgt0sr  10119  1re  10231  lelttr  10320  ltletr  10321  letr  10323  mul0or  10859  prodgt0  11060  mulge0b  11085  squeeze0  11118  sup2  11171  un0addcl  11518  un0mulcl  11519  nn0sub  11535  elnnz  11579  zindd  11670  rpneg  12056  xrlttri  12165  xrlelttr  12180  xrltletr  12181  xrletr  12182  qextlt  12227  qextle  12228  xmullem2  12288  xlemul1a  12311  xrsupexmnf  12328  xrinfmexpnf  12329  supxrun  12339  prunioo  12494  difreicc  12497  iccsplit  12498  uzsplit  12605  fzm1  12613  expcl2lem  13066  expeq0  13084  expnegz  13088  expaddz  13098  expmulz  13100  sqlecan  13165  facdiv  13268  facwordi  13270  bcpasc  13302  resqrex  14190  absexpz  14244  caubnd  14297  summo  14647  zsum  14648  zprod  14866  rpnnen2lem12  15153  ordvdsmul  15224  dvdsprime  15602  prmdvdsexpr  15631  prmfac1  15633  pythagtriplem2  15724  4sqlem11  15861  vdwlem6  15892  vdwlem9  15895  vdwlem13  15899  cshwshashlem3  16006  prmlem0  16014  xpscfv  16424  pleval2  17166  pltletr  17172  plelttr  17173  tsrlemax  17421  f1omvdco2  18068  psgnunilem2  18115  efgredlemc  18358  frgpuptinv  18384  lt6abl  18496  dmdprdsplit2lem  18644  drngmul0or  18970  lvecvs0or  19310  domneq0  19499  baspartn  20960  0top  20989  indistopon  21007  restntr  21188  cnindis  21298  cmpfi  21413  filconn  21888  ufprim  21914  ufildr  21936  alexsubALTlem2  22053  alexsubALTlem3  22054  alexsubALTlem4  22055  ovolicc2lem3  23487  rolle  23952  dvivthlem1  23970  coeaddlem  24204  dgrco  24230  plymul0or  24235  aalioulem3  24288  cxpge0  24628  cxpmul2z  24636  cxpcn3lem  24687  scvxcvx  24911  sqf11  25064  ppiublem1  25126  lgsdir2lem2  25250  lgsqrlem2  25271  lmieu  25875  upgrpredgv  26233  edglnl  26237  eucrct2eupth  27397  frgrogt3nreg  27565  nvmul0or  27814  hvmul0or  28191  disjxpin  29708  subfacp1lem4  31472  untsucf  31894  sotr3  31963  dfon2lem6  31998  dftrpred3g  32038  nosepon  32124  nolesgn2ores  32131  nosepne  32137  nolt02o  32151  nosupbnd1lem5  32164  broutsideof2  32535  btwnoutside  32538  broutsideof3  32539  outsideoftr  32542  lineunray  32560  lineelsb2  32561  finminlem  32618  nn0prpw  32624  refssfne  32659  meran1  32716  ontgval  32736  ordcmp  32752  bj-sngltag  33277  bj-ismooredr2  33371  topdifinfindis  33505  icoreclin  33516  finxpsuclem  33545  poimirlem24  33746  poimirlem25  33747  poimirlem29  33751  poimirlem31  33753  mblfinlem2  33760  ovoliunnfl  33764  itg2addnclem  33774  sdclem2  33851  fdc  33854  divrngidl  34140  lkreqN  34960  cvrnbtwn4  35069  4atlem12  35401  elpaddn0  35589  paddasslem17  35625  paddidm  35630  pmapjoin  35641  llnexchb2  35658  dalawlem13  35672  dalawlem14  35673  dochkrshp4  37180  lcfl6  37291  fphpdo  37883  pellfundex  37952  jm2.19lem4  38061  jm2.26a  38069  relexpmulg  38504  relexp01min  38507  relexpxpmin  38511  relexpaddss  38512  clsk1indlem3  38843  goldbachthlem2  41968  evenltle  42136  gbowge7  42161  bgoldbtbndlem3  42205  lidldomn1  42431  uzlidlring  42439
 Copyright terms: Public domain W3C validator