Theorem jaod 872

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

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 33	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 33	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 870	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 33	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  mpjaod  873  orel2  903  pm2.621  911  pm2.63  955  jaao  969  jaodan  972  ecase3d  1050  dedlema  1061  dedlemb  1062  cad0  1648  psssstr  4065  eqoreldif  4652  opthpr  4817  prel12g  4830  opthprneg  4831  axpr  5400  sotric  5601  sotr2  5605  sotr3  5612  relop  5838  suctr  6451  trsucss  6453  ordelinel  6466  fununi  6613  fnprb  7208  soisoi  7328  ordunisuc2  7841  poxp  8125  soxp  8126  frrlem12  8295  frrlem13  8296  tfrlem11  8376  omordi  8552  om00  8561  odi  8565  omeulem2  8569  oewordi  8578  nnmordi  8618  omsmolem  8644  swoord2  8729  nneneq  9191  dffi3  9392  inf3lem6  9603  cantnfle  9641  cantnflem1  9659  cantnflem2  9660  ttrcltr  9686  r1sdom  9747  r1ord3g  9752  rankxplim3  9854  carddom2  9964  wdomnumr  10049  alephordi  10059  alephdom  10066  cardaleph  10074  djuinf  10173  cfsuc  10242  cfsmolem  10255  sornom  10262  fin23lem25  10309  fin1a2lem11  10395  fin1a2s  10399  zorn2lem7  10487  ttukeylem5  10498  alephval2  10558  fpwwe2lem12  10628  gch2  10661  gchaclem  10664  prub  10980  sqgt0sr  11092  1re  11209  lelttr  11301  ltletr  11303  letr  11305  mul0or  11855  prodgt0  12063  mulge0b  12086  squeeze0  12119  sup2  12172  un0addcl  12538  un0mulcl  12539  nn0sub  12555  elnnz  12602  zindd  12698  rpneg  13051  xrlttri  13165  xrlelttr  13182  xrltletr  13183  xrletr  13184  qextlt  13230  qextle  13231  xmullem2  13292  xlemul1a  13315  xrsupexmnf  13332  xrinfmexpnf  13333  supxrun  13343  prunioo  13509  difreicc  13512  iccsplit  13513  uzsplit  13626  fzm1  13637  expcl2lem  14111  expeq0  14130  expnegz  14134  expaddz  14144  expmulz  14146  sqlecan  14247  facdiv  14325  facwordi  14327  bcpasc  14359  resqrex  15303  absexpz  15358  caubnd  15412  summo  15770  zsum  15771  zprod  15993  rpnnen2lem12  16282  ordvdsmul  16359  nn0rppwr  16620  nn0expgcd  16623  dvdsprime  16746  2mulprm  16752  ge2nprmge4  16761  prmdvdsexpr  16777  prmfac1  16780  pythagtriplem2  16878  4sqlem11  17016  vdwlem6  17047  vdwlem9  17050  vdwlem13  17054  cshwshashlem3  17158  prmlem0  17166  pleval2  18392  pltletr  18398  plelttr  18399  tsrlemax  18643  smndex1mgm  18970  f1omvdco2  19519  psgnunilem2  19566  efgredlemc  19816  frgpuptinv  19842  lt6abl  19966  dmdprdsplit2lem  20118  domneq0  20794  lvecvs0or  21213  unichnlidl  21343  baspartn  23092  0top  23121  indistopon  23139  restntr  23320  cnindis  23430  cmpfi  23546  filconn  24021  ufprim  24047  ufildr  24069  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALTlem4  24188  ovolicc2lem3  25659  rolle  26130  dvivthlem1  26148  coeaddlem  26387  dgrco  26413  plymul0or  26420  aalioulem3  26478  cxpge0  26829  cxpmul2z  26837  cxpcn3lem  26893  scvxcvx  27131  sqf11  27284  ppiublem1  27347  lgsdir2lem2  27471  lgsqrlem2  27492  2sqnn0  27583  2sqnn  27584  nosepon  27810  nolesgn2ores  27817  nogesgn1ores  27819  nosepne  27825  nolt02o  27840  nosupbnd1lem5  27857  madebdaylemlrcut  28073  madebday  28074  ltslpss  28082  addsproplem2  28144  leadds1  28163  addsuniflem  28175  mulsproplem9  28298  sltmuls1  28321  sltmuls2  28322  muls0ord  28359  precsexlem9  28389  precsexlem11  28391  recsex  28393  abssnid  28417  ltonold  28435  onnolt  28440  eucliddivs  28550  elnnzs  28575  expsne0  28610  bdaypw2n0bndlem  28637  bdayfinbndlem1  28641  z12zsodd  28656  lmieu  29074  upgrpredgv  29470  edglnl  29474  eucrct2eupth  30577  frgrogt3nreg  30729  nvmul0or  30983  hvmul0or  31358  snsssng  32841  disjxpin  32914  expgt0b  33142  axprALT2  35484  subfacp1lem4  35656  satfvsucsuc  35838  satfrnmapom  35843  sat1el2xp  35852  gonarlem  35867  gonar  35868  goalrlem  35869  goalr  35870  fmlasucdisj  35872  satffunlem1lem1  35875  satffunlem2lem1  35877  untsucf  36183  dfon2lem6  36259  broutsideof2  36595  btwnoutside  36598  broutsideof3  36599  outsideoftr  36602  lineunray  36620  lineelsb2  36621  nmuladdss  36671  ltnadd  36676  finminlem  36810  nn0prpw  36815  refssfne  36850  meran1  36903  ontgval  36923  ordcmp  36939  axtcond  36970  mh-inf3f1  37033  bj-sngltag  37600  bj-axseprep  37692  bj-prmoore  37738  topdifinfindis  37973  icoreclin  37984  rdgssun  38005  finxpsuclem  38024  poimirlem24  38276  poimirlem25  38277  poimirlem29  38281  poimirlem31  38283  mblfinlem2  38290  ovoliunnfl  38294  itg2addnclem  38303  sdclem2  38374  fdc  38377  divrngidl  38660  lkreqN  39925  cvrnbtwn4  40034  4atlem12  40367  elpaddn0  40555  paddasslem17  40591  paddidm  40596  pmapjoin  40607  llnexchb2  40624  dalawlem13  40638  dalawlem14  40639  dochkrshp4  42144  lcfl6  42255  lcmineqlem  42800  primrootspoweq0  42854  aks6d1c1  42864  sticksstones22  42916  aks6d1c6lem3  42920  oexpreposd  43064  expeqidd  43067  sn-remul0ord  43150  sn-sup2  43246  fphpdo  43527  pellfundex  43596  jm2.19lem4  43702  jm2.26a  43710  ordnexbtwnsuc  43977  onov0suclim  43984  oege2  44017  succlg  44038  dflim5  44039  oacl2g  44040  omcl2  44043  omcl3g  44044  naddgeoa  44104  safesnsupfiss  44124  fzunt  44164  fzuntd  44165  fzunt1d  44166  fzuntgd  44167  relexpmulg  44419  relexp01min  44422  relexpxpmin  44426  relexpaddss  44427  clsk1indlem3  44752  or2expropbi  47754  ich2exprop  48203  poprelb  48256  reuopreuprim  48258  goldbachthlem2  48281  nprmdvdsfacm1lem2  48356  nprmdvdsfacm1  48359  requad01  48369  evenltle  48465  gbowge7  48511  bgoldbtbndlem3  48555  elclnbgrelnbgr  48573  clnbgrel  48576  dfclnbgr6  48604  dfnbgr6  48605  dfsclnbgr6  48606  upgrimpths  48657  clnbgrgrim  48682  isubgr3stgrlem4  48717  isubgr3stgrlem7  48720  grlimgredgex  48748  gpgedgvtx1  48810  gpgvtxedg0  48811  gpgvtxedg1  48812  lidldomn1  48979  uzlidlring  48983  prelrrx2b  49477  line2y  49518  itschlc0xyqsol1  49529  itsclc0xyqsolr  49532  inlinecirc02plem  49549