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

Theorem jaod 853
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 851 . 2 ((𝜓𝜃) → (𝜑𝜒))
65com12 32 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841
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 208  df-or 842
This theorem is referenced by:  mpjaod  854  orel2  884  pm2.621  892  pm2.63  934  jaao  948  jaodan  951  ecase2d  1023  ecase3d  1026  dedlema  1037  dedlemb  1038  cad0  1609  psssstr  4080  eqoreldif  4614  opthpr  4774  prel12g  4786  opthprneg  4787  sotric  5494  sotr2  5498  relop  5714  suctr  6267  trsucss  6269  ordelinel  6282  fununi  6422  fnprb  6962  soisoi  7070  ordunisuc2  7548  poxp  7811  soxp  7812  wfrlem14  7957  wfrlem15  7958  tfrlem11  8013  omordi  8181  om00  8190  odi  8194  omeulem2  8198  oewordi  8206  nnmordi  8246  omsmolem  8269  swoord2  8310  nneneq  8688  dffi3  8883  inf3lem6  9084  cantnfle  9122  cantnflem1  9140  cantnflem2  9141  r1sdom  9191  r1ord3g  9196  rankxplim3  9298  carddom2  9394  wdomnumr  9478  alephordi  9488  alephdom  9495  cardaleph  9503  djuinf  9602  cfsuc  9667  cfsmolem  9680  sornom  9687  fin23lem25  9734  fin1a2lem11  9820  fin1a2s  9824  zorn2lem7  9912  ttukeylem5  9923  alephval2  9982  fpwwe2lem13  10052  gch2  10085  gchaclem  10088  prub  10404  sqgt0sr  10516  1re  10629  lelttr  10719  ltletr  10720  letr  10722  mul0or  11268  prodgt0  11475  mulge0b  11498  squeeze0  11531  sup2  11585  nnne0  11659  un0addcl  11918  un0mulcl  11919  nn0sub  11935  elnnz  11979  zindd  12071  rpneg  12409  xrlttri  12520  xrlelttr  12537  xrltletr  12538  xrletr  12539  qextlt  12584  qextle  12585  xmullem2  12646  xlemul1a  12669  xrsupexmnf  12686  xrinfmexpnf  12687  supxrun  12697  prunioo  12855  difreicc  12858  iccsplit  12859  uzsplit  12967  fzm1  12975  expcl2lem  13429  expeq0  13447  expnegz  13451  expaddz  13461  expmulz  13463  sqlecan  13559  facdiv  13635  facwordi  13637  bcpasc  13669  resqrex  14598  absexpz  14653  caubnd  14706  summo  15062  zsum  15063  zprod  15279  rpnnen2lem12  15566  ordvdsmul  15638  dvdsprime  16019  2mulprm  16025  ge2nprmge4  16033  prmdvdsexpr  16049  prmfac1  16051  pythagtriplem2  16142  4sqlem11  16279  vdwlem6  16310  vdwlem9  16313  vdwlem13  16317  cshwshashlem3  16419  prmlem0  16427  pleval2  17563  pltletr  17569  plelttr  17570  tsrlemax  17818  f1omvdco2  18505  psgnunilem2  18552  efgredlemc  18800  frgpuptinv  18826  lt6abl  18944  dmdprdsplit2lem  19096  drngmul0or  19452  lvecvs0or  19809  domneq0  19998  baspartn  21490  0top  21519  indistopon  21537  restntr  21718  cnindis  21828  cmpfi  21944  filconn  22419  ufprim  22445  ufildr  22467  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALTlem4  22586  ovolicc2lem3  24047  rolle  24514  dvivthlem1  24532  coeaddlem  24766  dgrco  24792  plymul0or  24797  aalioulem3  24850  cxpge0  25193  cxpmul2z  25201  cxpcn3lem  25255  scvxcvx  25490  sqf11  25643  ppiublem1  25705  lgsdir2lem2  25829  lgsqrlem2  25850  2sqnn0  25941  2sqnn  25942  lmieu  26497  upgrpredgv  26851  edglnl  26855  eucrct2eupth  27951  frgrogt3nreg  28103  nvmul0or  28354  hvmul0or  28729  disjxpin  30266  subfacp1lem4  32327  satfvsucsuc  32509  satfrnmapom  32514  sat1el2xp  32523  gonarlem  32538  gonar  32539  goalrlem  32540  goalr  32541  fmlasucdisj  32543  satffunlem1lem1  32546  satffunlem2lem1  32548  untsucf  32833  sotr3  32899  dfon2lem6  32930  dftrpred3g  32969  frrlem12  33031  frrlem13  33032  nosepon  33069  nolesgn2ores  33076  nosepne  33082  nolt02o  33096  nosupbnd1lem5  33109  broutsideof2  33480  btwnoutside  33483  broutsideof3  33484  outsideoftr  33487  lineunray  33505  lineelsb2  33506  finminlem  33563  nn0prpw  33568  refssfne  33603  meran1  33656  ontgval  33676  ordcmp  33692  bj-sngltag  34192  topdifinfindis  34509  icoreclin  34520  rdgssun  34541  finxpsuclem  34560  poimirlem24  34797  poimirlem25  34798  poimirlem29  34802  poimirlem31  34804  mblfinlem2  34811  ovoliunnfl  34815  itg2addnclem  34824  sdclem2  34898  fdc  34901  divrngidl  35187  lkreqN  36186  cvrnbtwn4  36295  4atlem12  36628  elpaddn0  36816  paddasslem17  36852  paddidm  36857  pmapjoin  36868  llnexchb2  36885  dalawlem13  36899  dalawlem14  36900  dochkrshp4  38405  lcfl6  38516  oexpreposd  39057  nn0rppwr  39060  nn0expgcd  39062  fphpdo  39292  pellfundex  39361  jm2.19lem4  39467  jm2.26a  39475  relexpmulg  39933  relexp01min  39936  relexpxpmin  39940  relexpaddss  39941  clsk1indlem3  40271  or2expropbi  43146  ich2exprop  43510  poprelb  43563  reuopreuprim  43565  goldbachthlem2  43585  requad01  43663  evenltle  43759  gbowge7  43805  bgoldbtbndlem3  43849  smndex1mgm  44007  lidldomn1  44120  uzlidlring  44128  prelrrx2b  44629  line2y  44670  itschlc0xyqsol1  44681  itsclc0xyqsolr  44684  inlinecirc02plem  44701
  Copyright terms: Public domain W3C validator