Theorem jaod 856

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 32	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 32	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 854	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  mpjaod  857  orel2  888  pm2.621  896  pm2.63  938  jaao  952  jaodan  955  ecase2dOLD  1028  ecase3d  1031  dedlema  1043  dedlemb  1044  cad0  1620  cad0OLD  1621  psssstr  4042  eqoreldif  4621  opthpr  4783  prel12g  4795  opthprneg  4796  sotric  5532  sotr2  5536  relop  5762  suctr  6353  trsucss  6355  ordelinel  6368  fununi  6516  fnprb  7093  soisoi  7208  ordunisuc2  7700  poxp  7978  soxp  7979  frrlem12  8122  frrlem13  8123  wfrlem14OLD  8162  wfrlem15OLD  8163  tfrlem11  8228  omordi  8406  om00  8415  odi  8419  omeulem2  8423  oewordi  8431  nnmordi  8471  omsmolem  8496  swoord2  8539  nneneq  9001  nneneqOLD  9013  dffi3  9199  inf3lem6  9400  cantnfle  9438  cantnflem1  9456  cantnflem2  9457  ttrcltr  9483  r1sdom  9541  r1ord3g  9546  rankxplim3  9648  carddom2  9744  wdomnumr  9829  alephordi  9839  alephdom  9846  cardaleph  9854  djuinf  9953  cfsuc  10022  cfsmolem  10035  sornom  10042  fin23lem25  10089  fin1a2lem11  10175  fin1a2s  10179  zorn2lem7  10267  ttukeylem5  10278  alephval2  10337  fpwwe2lem12  10407  gch2  10440  gchaclem  10443  prub  10759  sqgt0sr  10871  1re  10984  lelttr  11074  ltletr  11076  letr  11078  mul0or  11624  prodgt0  11831  mulge0b  11854  squeeze0  11887  sup2  11940  nnne0  12016  un0addcl  12275  un0mulcl  12276  nn0sub  12292  elnnz  12338  zindd  12430  rpneg  12771  xrlttri  12882  xrlelttr  12899  xrltletr  12900  xrletr  12901  qextlt  12946  qextle  12947  xmullem2  13008  xlemul1a  13031  xrsupexmnf  13048  xrinfmexpnf  13049  supxrun  13059  prunioo  13222  difreicc  13225  iccsplit  13226  uzsplit  13337  fzm1  13345  expcl2lem  13803  expeq0  13822  expnegz  13826  expaddz  13836  expmulz  13838  sqlecan  13934  facdiv  14010  facwordi  14012  bcpasc  14044  resqrex  14971  absexpz  15026  caubnd  15079  summo  15438  zsum  15439  zprod  15656  rpnnen2lem12  15943  ordvdsmul  16018  dvdsprime  16401  2mulprm  16407  ge2nprmge4  16415  prmdvdsexpr  16431  prmfac1  16435  pythagtriplem2  16527  4sqlem11  16665  vdwlem6  16696  vdwlem9  16699  vdwlem13  16703  cshwshashlem3  16808  prmlem0  16816  pleval2  18064  pltletr  18070  plelttr  18071  tsrlemax  18313  smndex1mgm  18555  f1omvdco2  19065  psgnunilem2  19112  efgredlemc  19360  frgpuptinv  19386  lt6abl  19505  dmdprdsplit2lem  19657  drngmul0or  20021  lvecvs0or  20379  domneq0  20577  baspartn  22113  0top  22142  indistopon  22160  restntr  22342  cnindis  22452  cmpfi  22568  filconn  23043  ufprim  23069  ufildr  23091  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  ovolicc2lem3  24692  rolle  25163  dvivthlem1  25181  coeaddlem  25419  dgrco  25445  plymul0or  25450  aalioulem3  25503  cxpge0  25847  cxpmul2z  25855  cxpcn3lem  25909  scvxcvx  26144  sqf11  26297  ppiublem1  26359  lgsdir2lem2  26483  lgsqrlem2  26504  2sqnn0  26595  2sqnn  26596  lmieu  27154  upgrpredgv  27518  edglnl  27522  eucrct2eupth  28618  frgrogt3nreg  28770  nvmul0or  29021  hvmul0or  29396  snsssng  30869  disjxpin  30936  subfacp1lem4  33154  satfvsucsuc  33336  satfrnmapom  33341  sat1el2xp  33350  gonarlem  33365  gonar  33366  goalrlem  33367  goalr  33368  fmlasucdisj  33370  satffunlem1lem1  33373  satffunlem2lem1  33375  untsucf  33660  sotr3  33742  dfon2lem6  33773  nosepon  33877  nolesgn2ores  33884  nogesgn1ores  33886  nosepne  33892  nolt02o  33907  nosupbnd1lem5  33924  madebdaylemlrcut  34088  madebday  34089  sltlpss  34096  broutsideof2  34433  btwnoutside  34436  broutsideof3  34437  outsideoftr  34440  lineunray  34458  lineelsb2  34459  finminlem  34516  nn0prpw  34521  refssfne  34556  meran1  34609  ontgval  34629  ordcmp  34645  bj-sngltag  35182  bj-prmoore  35295  topdifinfindis  35526  icoreclin  35537  rdgssun  35558  finxpsuclem  35577  poimirlem24  35810  poimirlem25  35811  poimirlem29  35815  poimirlem31  35817  mblfinlem2  35824  ovoliunnfl  35828  itg2addnclem  35837  sdclem2  35909  fdc  35912  divrngidl  36195  lkreqN  37191  cvrnbtwn4  37300  4atlem12  37633  elpaddn0  37821  paddasslem17  37857  paddidm  37862  pmapjoin  37873  llnexchb2  37890  dalawlem13  37904  dalawlem14  37905  dochkrshp4  39410  lcfl6  39521  lcmineqlem  40067  sticksstones22  40131  oexpreposd  40328  nn0rppwr  40340  nn0expgcd  40342  sn-sup2  40446  fphpdo  40646  pellfundex  40715  jm2.19lem4  40821  jm2.26a  40829  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  relexpmulg  41325  relexp01min  41328  relexpxpmin  41332  relexpaddss  41333  clsk1indlem3  41660  or2expropbi  44539  ich2exprop  44934  poprelb  44987  reuopreuprim  44989  goldbachthlem2  45009  requad01  45084  evenltle  45180  gbowge7  45226  bgoldbtbndlem3  45270  lidldomn1  45490  uzlidlring  45498  prelrrx2b  46071  line2y  46112  itschlc0xyqsol1  46123  itsclc0xyqsolr  46126  inlinecirc02plem  46143