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

Theorem jaod 855
 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 853 . 2 ((𝜓𝜃) → (𝜑𝜒))
65com12 32 1 (𝜑 → ((𝜓𝜃) → 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 843 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 209  df-or 844 This theorem is referenced by:  mpjaod  856  orel2  887  pm2.621  895  pm2.63  937  jaao  951  jaodan  954  ecase2d  1026  ecase3d  1029  dedlema  1040  dedlemb  1041  cad0  1614  psssstr  4083  eqoreldif  4616  opthpr  4776  prel12g  4788  opthprneg  4789  sotric  5496  sotr2  5500  relop  5716  suctr  6269  trsucss  6271  ordelinel  6284  fununi  6424  fnprb  6965  soisoi  7075  ordunisuc2  7553  poxp  7816  soxp  7817  wfrlem14  7962  wfrlem15  7963  tfrlem11  8018  omordi  8186  om00  8195  odi  8199  omeulem2  8203  oewordi  8211  nnmordi  8251  omsmolem  8274  swoord2  8315  nneneq  8694  dffi3  8889  inf3lem6  9090  cantnfle  9128  cantnflem1  9146  cantnflem2  9147  r1sdom  9197  r1ord3g  9202  rankxplim3  9304  carddom2  9400  wdomnumr  9484  alephordi  9494  alephdom  9501  cardaleph  9509  djuinf  9608  cfsuc  9673  cfsmolem  9686  sornom  9693  fin23lem25  9740  fin1a2lem11  9826  fin1a2s  9830  zorn2lem7  9918  ttukeylem5  9929  alephval2  9988  fpwwe2lem13  10058  gch2  10091  gchaclem  10094  prub  10410  sqgt0sr  10522  1re  10635  lelttr  10725  ltletr  10726  letr  10728  mul0or  11274  prodgt0  11481  mulge0b  11504  squeeze0  11537  sup2  11591  nnne0  11665  un0addcl  11924  un0mulcl  11925  nn0sub  11941  elnnz  11985  zindd  12077  rpneg  12415  xrlttri  12526  xrlelttr  12543  xrltletr  12544  xrletr  12545  qextlt  12590  qextle  12591  xmullem2  12652  xlemul1a  12675  xrsupexmnf  12692  xrinfmexpnf  12693  supxrun  12703  prunioo  12861  difreicc  12864  iccsplit  12865  uzsplit  12973  fzm1  12981  expcl2lem  13435  expeq0  13453  expnegz  13457  expaddz  13467  expmulz  13469  sqlecan  13565  facdiv  13641  facwordi  13643  bcpasc  13675  resqrex  14604  absexpz  14659  caubnd  14712  summo  15068  zsum  15069  zprod  15285  rpnnen2lem12  15572  ordvdsmul  15644  dvdsprime  16025  2mulprm  16031  ge2nprmge4  16039  prmdvdsexpr  16055  prmfac1  16057  pythagtriplem2  16148  4sqlem11  16285  vdwlem6  16316  vdwlem9  16319  vdwlem13  16323  cshwshashlem3  16425  prmlem0  16433  pleval2  17569  pltletr  17575  plelttr  17576  tsrlemax  17824  smndex1mgm  18066  f1omvdco2  18570  psgnunilem2  18617  efgredlemc  18865  frgpuptinv  18891  lt6abl  19009  dmdprdsplit2lem  19161  drngmul0or  19517  lvecvs0or  19874  domneq0  20064  baspartn  21556  0top  21585  indistopon  21603  restntr  21784  cnindis  21894  cmpfi  22010  filconn  22485  ufprim  22511  ufildr  22533  alexsubALTlem2  22650  alexsubALTlem3  22651  alexsubALTlem4  22652  ovolicc2lem3  24114  rolle  24581  dvivthlem1  24599  coeaddlem  24833  dgrco  24859  plymul0or  24864  aalioulem3  24917  cxpge0  25260  cxpmul2z  25268  cxpcn3lem  25322  scvxcvx  25557  sqf11  25710  ppiublem1  25772  lgsdir2lem2  25896  lgsqrlem2  25917  2sqnn0  26008  2sqnn  26009  lmieu  26564  upgrpredgv  26918  edglnl  26922  eucrct2eupth  28018  frgrogt3nreg  28170  nvmul0or  28421  hvmul0or  28796  disjxpin  30332  subfacp1lem4  32425  satfvsucsuc  32607  satfrnmapom  32612  sat1el2xp  32621  gonarlem  32636  gonar  32637  goalrlem  32638  goalr  32639  fmlasucdisj  32641  satffunlem1lem1  32644  satffunlem2lem1  32646  untsucf  32931  sotr3  32997  dfon2lem6  33028  dftrpred3g  33067  frrlem12  33129  frrlem13  33130  nosepon  33167  nolesgn2ores  33174  nosepne  33180  nolt02o  33194  nosupbnd1lem5  33207  broutsideof2  33578  btwnoutside  33581  broutsideof3  33582  outsideoftr  33585  lineunray  33603  lineelsb2  33604  finminlem  33661  nn0prpw  33666  refssfne  33701  meran1  33754  ontgval  33774  ordcmp  33790  bj-sngltag  34290  bj-prmoore  34401  topdifinfindis  34621  icoreclin  34632  rdgssun  34653  finxpsuclem  34672  poimirlem24  34910  poimirlem25  34911  poimirlem29  34915  poimirlem31  34917  mblfinlem2  34924  ovoliunnfl  34928  itg2addnclem  34937  sdclem2  35011  fdc  35014  divrngidl  35300  lkreqN  36300  cvrnbtwn4  36409  4atlem12  36742  elpaddn0  36930  paddasslem17  36966  paddidm  36971  pmapjoin  36982  llnexchb2  36999  dalawlem13  37013  dalawlem14  37014  dochkrshp4  38519  lcfl6  38630  oexpreposd  39172  nn0rppwr  39175  nn0expgcd  39177  fphpdo  39407  pellfundex  39476  jm2.19lem4  39582  jm2.26a  39590  relexpmulg  40048  relexp01min  40051  relexpxpmin  40055  relexpaddss  40056  clsk1indlem3  40386  or2expropbi  43262  ich2exprop  43626  poprelb  43679  reuopreuprim  43681  goldbachthlem2  43701  requad01  43779  evenltle  43875  gbowge7  43921  bgoldbtbndlem3  43965  lidldomn1  44185  uzlidlring  44193  prelrrx2b  44694  line2y  44735  itschlc0xyqsol1  44746  itsclc0xyqsolr  44749  inlinecirc02plem  44766
 Copyright terms: Public domain W3C validator