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

Theorem jaod 885
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 883 . 2 ((𝜓𝜃) → (𝜑𝜒))
65com12 32 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 873
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 198  df-or 874
This theorem is referenced by:  mpjaod  886  orel2  914  pm2.621  922  pm2.63  964  jaao  977  jaodan  980  ecase2d  1054  ecase3d  1057  dedlema  1068  dedlemb  1069  cad0  1726  psssstr  3874  eqoreldif  4382  opthpr  4535  prel12g  4550  opthprneg  4551  sotric  5224  sotr2  5227  relop  5441  suctr  5991  trsucss  5993  ordelinel  6006  fununi  6142  fnprb  6665  soisoi  6770  ordunisuc2  7242  poxp  7491  soxp  7492  wfrlem14  7632  wfrlem15  7633  tfrlem11  7688  omordi  7851  om00  7860  odi  7864  omeulem2  7868  oewordi  7876  nnmordi  7916  omsmolem  7938  swoord2  7979  nneneq  8350  dffi3  8544  inf3lem6  8745  cantnfle  8783  cantnflem1  8801  cantnflem2  8802  r1sdom  8852  r1ord3g  8857  rankxplim3  8959  carddom2  9054  wdomnumr  9138  alephordi  9148  alephdom  9155  cardaleph  9163  cdainf  9267  cfsuc  9332  cfsmolem  9345  sornom  9352  fin23lem25  9399  fin1a2lem11  9485  fin1a2s  9489  zorn2lem7  9577  ttukeylem5  9588  alephval2  9647  fpwwe2lem13  9717  gch2  9750  gchaclem  9753  prub  10069  sqgt0sr  10180  1re  10293  lelttr  10382  ltletr  10383  letr  10385  mul0or  10921  prodgt0  11122  mulge0b  11147  squeeze0  11180  sup2  11233  un0addcl  11573  un0mulcl  11574  nn0sub  11590  elnnz  11634  zindd  11725  rpneg  12061  xrlttri  12172  xrlelttr  12189  xrltletr  12190  xrletr  12191  qextlt  12236  qextle  12237  xmullem2  12297  xlemul1a  12320  xrsupexmnf  12337  xrinfmexpnf  12338  supxrun  12348  prunioo  12508  difreicc  12511  iccsplit  12512  uzsplit  12619  fzm1  12627  expcl2lem  13079  expeq0  13097  expnegz  13101  expaddz  13111  expmulz  13113  sqlecan  13178  facdiv  13278  facwordi  13280  bcpasc  13312  resqrex  14276  absexpz  14330  caubnd  14383  summo  14733  zsum  14734  zprod  14950  rpnnen2lem12  15236  ordvdsmul  15307  dvdsprime  15680  prmdvdsexpr  15708  prmfac1  15710  pythagtriplem2  15801  4sqlem11  15938  vdwlem6  15969  vdwlem9  15972  vdwlem13  15976  cshwshashlem3  16078  prmlem0  16086  xpscfv  16488  pleval2  17231  pltletr  17237  plelttr  17238  tsrlemax  17486  f1omvdco2  18131  psgnunilem2  18179  efgredlemc  18423  frgpuptinv  18450  lt6abl  18562  dmdprdsplit2lem  18711  drngmul0or  19037  lvecvs0or  19380  domneq0  19571  baspartn  21038  0top  21067  indistopon  21085  restntr  21266  cnindis  21376  cmpfi  21491  filconn  21966  ufprim  21992  ufildr  22014  alexsubALTlem2  22131  alexsubALTlem3  22132  alexsubALTlem4  22133  ovolicc2lem3  23577  rolle  24044  dvivthlem1  24062  coeaddlem  24296  dgrco  24322  plymul0or  24327  aalioulem3  24380  cxpge0  24720  cxpmul2z  24728  cxpcn3lem  24779  scvxcvx  25003  sqf11  25156  ppiublem1  25218  lgsdir2lem2  25342  lgsqrlem2  25363  lmieu  25967  upgrpredgv  26312  edglnl  26316  eucrct2eupth  27523  frgrogt3nreg  27713  nvmul0or  27961  hvmul0or  28338  disjxpin  29849  subfacp1lem4  31613  untsucf  32033  sotr3  32101  dfon2lem6  32136  dftrpred3g  32176  nosepon  32262  nolesgn2ores  32269  nosepne  32275  nolt02o  32289  nosupbnd1lem5  32302  broutsideof2  32673  btwnoutside  32676  broutsideof3  32677  outsideoftr  32680  lineunray  32698  lineelsb2  32699  finminlem  32756  nn0prpw  32761  refssfne  32796  meran1  32849  ontgval  32869  ordcmp  32885  bj-sngltag  33398  bj-ismooredr2  33493  topdifinfindis  33627  icoreclin  33638  finxpsuclem  33667  poimirlem24  33857  poimirlem25  33858  poimirlem29  33862  poimirlem31  33864  mblfinlem2  33871  ovoliunnfl  33875  itg2addnclem  33884  sdclem2  33960  fdc  33963  divrngidl  34249  lkreqN  35126  cvrnbtwn4  35235  4atlem12  35568  elpaddn0  35756  paddasslem17  35792  paddidm  35797  pmapjoin  35808  llnexchb2  35825  dalawlem13  35839  dalawlem14  35840  dochkrshp4  37345  lcfl6  37456  fphpdo  38059  pellfundex  38128  jm2.19lem4  38236  jm2.26a  38244  relexpmulg  38677  relexp01min  38680  relexpxpmin  38684  relexpaddss  38685  clsk1indlem3  39015  goldbachthlem2  42134  evenltle  42302  gbowge7  42327  bgoldbtbndlem3  42371  lidldomn1  42590  uzlidlring  42598
  Copyright terms: Public domain W3C validator