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

Theorem jaod 395
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 394 . 2 ((𝜓𝜃) → (𝜑𝜒))
65com12 32 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383
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 385
This theorem is referenced by:  mpjaod  396  orel2  398  pm2.621  424  jaao  531  jaodan  825  pm2.63  828  ecase2d  980  ecase3d  983  dedlema  1001  dedlemb  1002  cad0  1553  psssstr  3697  eqoreldif  4203  opthpr  4359  sotric  5031  sotr2  5034  relop  5242  suctr  5777  trsucss  5780  ordelinel  5794  ordelinelOLD  5795  fununi  5932  fnprb  6437  soisoi  6543  ordunisuc2  7006  poxp  7249  soxp  7250  wfrlem14  7388  wfrlem15  7389  tfrlem11  7444  omordi  7606  om00  7615  odi  7619  omeulem2  7623  oewordi  7631  nnmordi  7671  omsmolem  7693  swoord2  7734  nneneq  8103  dffi3  8297  inf3lem6  8490  cantnfle  8528  cantnflem1  8546  cantnflem2  8547  r1sdom  8597  r1ord3g  8602  rankxplim3  8704  carddom2  8763  wdomnumr  8847  alephordi  8857  alephdom  8864  cardaleph  8872  cdainf  8974  cfsuc  9039  cfsmolem  9052  sornom  9059  fin23lem25  9106  fin1a2lem11  9192  fin1a2s  9196  zorn2lem7  9284  ttukeylem5  9295  alephval2  9354  fpwwe2lem13  9424  gch2  9457  gchaclem  9460  prub  9776  sqgt0sr  9887  1re  9999  lelttr  10088  ltletr  10089  letr  10091  mul0or  10627  prodgt0  10828  mulge0b  10853  squeeze0  10886  sup2  10939  un0addcl  11286  un0mulcl  11287  nn0sub  11303  elnnz  11347  zindd  11438  rpneg  11823  xrlttri  11932  xrlelttr  11947  xrltletr  11948  xrletr  11949  qextlt  11993  qextle  11994  xmullem2  12054  xlemul1a  12077  xrsupexmnf  12094  xrinfmexpnf  12095  supxrun  12105  prunioo  12259  difreicc  12262  iccsplit  12263  uzsplit  12369  fzm1  12377  expcl2lem  12828  expeq0  12846  expnegz  12850  expaddz  12860  expmulz  12862  sqlecan  12927  facdiv  13030  facwordi  13032  bcpasc  13064  resqrex  13941  absexpz  13995  caubnd  14048  summo  14397  zsum  14398  zprod  14611  rpnnen2lem12  14898  ordvdsmul  14965  dvdsprime  15343  prmdvdsexpr  15372  prmfac1  15374  pythagtriplem2  15465  4sqlem11  15602  vdwlem6  15633  vdwlem9  15636  vdwlem13  15640  cshwshashlem3  15747  prmlem0  15755  xpscfv  16162  pleval2  16905  pltletr  16911  plelttr  16912  tsrlemax  17160  f1omvdco2  17808  psgnunilem2  17855  efgredlemc  18098  frgpuptinv  18124  lt6abl  18236  dmdprdsplit2lem  18384  drngmul0or  18708  lvecvs0or  19048  domneq0  19237  baspartn  20698  0top  20727  indistopon  20745  restntr  20926  cnindis  21036  cmpfi  21151  filconn  21627  ufprim  21653  ufildr  21675  alexsubALTlem2  21792  alexsubALTlem3  21793  alexsubALTlem4  21794  ovolicc2lem3  23227  rolle  23691  dvivthlem1  23709  coeaddlem  23943  dgrco  23969  plymul0or  23974  aalioulem3  24027  cxpge0  24363  cxpmul2z  24371  cxpcn3lem  24422  scvxcvx  24646  sqf11  24799  ppiublem1  24861  lgsdir2lem2  24985  lgsqrlem2  25006  lmieu  25610  upgrpredgv  25963  eucrct2eupth  27005  frgrogt3nreg  27143  nvmul0or  27393  hvmul0or  27770  disjxpin  29287  subfacp1lem4  30926  untsucf  31348  sotr3  31418  dfon2lem6  31447  dftrpred3g  31487  nosepon  31576  slttr2  31588  slttr3  31589  nodenselem4  31600  nosepne  31619  broutsideof2  31924  btwnoutside  31927  broutsideof3  31928  outsideoftr  31931  lineunray  31949  lineelsb2  31950  finminlem  32007  nn0prpw  32013  refssfne  32048  meran1  32105  ontgval  32125  ordcmp  32141  bj-sngltag  32671  topdifinfindis  32865  icoreclin  32876  finxpsuclem  32905  poimirlem24  33104  poimirlem25  33105  poimirlem29  33109  poimirlem31  33111  mblfinlem2  33118  ovoliunnfl  33122  itg2addnclem  33132  sdclem2  33209  fdc  33212  divrngidl  33498  lkreqN  33976  cvrnbtwn4  34085  4atlem12  34417  elpaddn0  34605  paddasslem17  34641  paddidm  34646  pmapjoin  34657  llnexchb2  34674  dalawlem13  34688  dalawlem14  34689  dochkrshp4  36197  lcfl6  36308  fphpdo  36900  pellfundex  36969  jm2.19lem4  37078  jm2.26a  37086  relexpmulg  37522  relexp01min  37525  relexpxpmin  37529  relexpaddss  37530  clsk1indlem3  37862  goldbachthlem2  40787  gboge7  40976  bgoldbtbndlem3  41014  lidldomn1  41239  uzlidlring  41247
  Copyright terms: Public domain W3C validator