MPE Home 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  530  jaodan  843  pm2.63  846  ecase2d  1000  ecase3d  1003  dedlema  1014  dedlemb  1015  cad0  1596  psssstr  3746  eqoreldif  4257  opthpr  4415  sotric  5090  sotr2  5093  relop  5305  suctr  5846  trsucss  5849  ordelinel  5863  ordelinelOLD  5864  fununi  6002  fnprb  6513  soisoi  6618  ordunisuc2  7086  poxp  7334  soxp  7335  wfrlem14  7473  wfrlem15  7474  tfrlem11  7529  omordi  7691  om00  7700  odi  7704  omeulem2  7708  oewordi  7716  nnmordi  7756  omsmolem  7778  swoord2  7819  nneneq  8184  dffi3  8378  inf3lem6  8568  cantnfle  8606  cantnflem1  8624  cantnflem2  8625  r1sdom  8675  r1ord3g  8680  rankxplim3  8782  carddom2  8841  wdomnumr  8925  alephordi  8935  alephdom  8942  cardaleph  8950  cdainf  9052  cfsuc  9117  cfsmolem  9130  sornom  9137  fin23lem25  9184  fin1a2lem11  9270  fin1a2s  9274  zorn2lem7  9362  ttukeylem5  9373  alephval2  9432  fpwwe2lem13  9502  gch2  9535  gchaclem  9538  prub  9854  sqgt0sr  9965  1re  10077  lelttr  10166  ltletr  10167  letr  10169  mul0or  10705  prodgt0  10906  mulge0b  10931  squeeze0  10964  sup2  11017  un0addcl  11364  un0mulcl  11365  nn0sub  11381  elnnz  11425  zindd  11516  rpneg  11901  xrlttri  12010  xrlelttr  12025  xrltletr  12026  xrletr  12027  qextlt  12072  qextle  12073  xmullem2  12133  xlemul1a  12156  xrsupexmnf  12173  xrinfmexpnf  12174  supxrun  12184  prunioo  12339  difreicc  12342  iccsplit  12343  uzsplit  12450  fzm1  12458  expcl2lem  12912  expeq0  12930  expnegz  12934  expaddz  12944  expmulz  12946  sqlecan  13011  facdiv  13114  facwordi  13116  bcpasc  13148  resqrex  14035  absexpz  14089  caubnd  14142  summo  14492  zsum  14493  zprod  14711  rpnnen2lem12  14998  ordvdsmul  15069  dvdsprime  15447  prmdvdsexpr  15476  prmfac1  15478  pythagtriplem2  15569  4sqlem11  15706  vdwlem6  15737  vdwlem9  15740  vdwlem13  15744  cshwshashlem3  15851  prmlem0  15859  xpscfv  16269  pleval2  17012  pltletr  17018  plelttr  17019  tsrlemax  17267  f1omvdco2  17914  psgnunilem2  17961  efgredlemc  18204  frgpuptinv  18230  lt6abl  18342  dmdprdsplit2lem  18490  drngmul0or  18816  lvecvs0or  19156  domneq0  19345  baspartn  20806  0top  20835  indistopon  20853  restntr  21034  cnindis  21144  cmpfi  21259  filconn  21734  ufprim  21760  ufildr  21782  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  ovolicc2lem3  23333  rolle  23798  dvivthlem1  23816  coeaddlem  24050  dgrco  24076  plymul0or  24081  aalioulem3  24134  cxpge0  24474  cxpmul2z  24482  cxpcn3lem  24533  scvxcvx  24757  sqf11  24910  ppiublem1  24972  lgsdir2lem2  25096  lgsqrlem2  25117  lmieu  25721  upgrpredgv  26079  edglnl  26083  eucrct2eupth  27223  frgrogt3nreg  27384  nvmul0or  27633  hvmul0or  28010  disjxpin  29527  subfacp1lem4  31291  untsucf  31713  sotr3  31782  dfon2lem6  31817  dftrpred3g  31857  nosepon  31943  nolesgn2ores  31950  nosepne  31956  nolt02o  31970  nosupbnd1lem5  31983  broutsideof2  32354  btwnoutside  32357  broutsideof3  32358  outsideoftr  32361  lineunray  32379  lineelsb2  32380  finminlem  32437  nn0prpw  32443  refssfne  32478  meran1  32535  ontgval  32555  ordcmp  32571  bj-sngltag  33096  bj-ismooredr2  33190  topdifinfindis  33324  icoreclin  33335  finxpsuclem  33364  poimirlem24  33563  poimirlem25  33564  poimirlem29  33568  poimirlem31  33570  mblfinlem2  33577  ovoliunnfl  33581  itg2addnclem  33591  sdclem2  33668  fdc  33671  divrngidl  33957  lkreqN  34775  cvrnbtwn4  34884  4atlem12  35216  elpaddn0  35404  paddasslem17  35440  paddidm  35445  pmapjoin  35456  llnexchb2  35473  dalawlem13  35487  dalawlem14  35488  dochkrshp4  36995  lcfl6  37106  fphpdo  37698  pellfundex  37767  jm2.19lem4  37876  jm2.26a  37884  relexpmulg  38319  relexp01min  38322  relexpxpmin  38326  relexpaddss  38327  clsk1indlem3  38658  goldbachthlem2  41783  evenltle  41951  gbowge7  41976  bgoldbtbndlem3  42020  lidldomn1  42246  uzlidlring  42254
  Copyright terms: Public domain W3C validator