Theorem jaod 860

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 858	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  mpjaod  861  orel2  891  pm2.621  899  pm2.63  943  jaao  957  jaodan  960  ecase3d  1035  dedlema  1046  dedlemb  1047  cad0  1618  psssstr  4109  eqoreldif  4685  opthpr  4851  prel12g  4864  opthprneg  4865  axpr  5427  sotric  5622  sotr2  5626  sotr3  5633  relop  5861  suctr  6470  trsucss  6472  ordelinel  6485  fununi  6641  fnprb  7228  soisoi  7348  ordunisuc2  7865  poxp  8153  soxp  8154  frrlem12  8322  frrlem13  8323  wfrlem14OLD  8362  wfrlem15OLD  8363  tfrlem11  8428  omordi  8604  om00  8613  odi  8617  omeulem2  8621  oewordi  8629  nnmordi  8669  omsmolem  8695  swoord2  8778  nneneq  9246  nneneqOLD  9258  dffi3  9471  inf3lem6  9673  cantnfle  9711  cantnflem1  9729  cantnflem2  9730  ttrcltr  9756  r1sdom  9814  r1ord3g  9819  rankxplim3  9921  carddom2  10017  wdomnumr  10104  alephordi  10114  alephdom  10121  cardaleph  10129  djuinf  10229  cfsuc  10297  cfsmolem  10310  sornom  10317  fin23lem25  10364  fin1a2lem11  10450  fin1a2s  10454  zorn2lem7  10542  ttukeylem5  10553  alephval2  10612  fpwwe2lem12  10682  gch2  10715  gchaclem  10718  prub  11034  sqgt0sr  11146  1re  11261  lelttr  11351  ltletr  11353  letr  11355  mul0or  11903  prodgt0  12114  mulge0b  12138  squeeze0  12171  sup2  12224  un0addcl  12559  un0mulcl  12560  nn0sub  12576  elnnz  12623  zindd  12719  rpneg  13067  xrlttri  13181  xrlelttr  13198  xrltletr  13199  xrletr  13200  qextlt  13245  qextle  13246  xmullem2  13307  xlemul1a  13330  xrsupexmnf  13347  xrinfmexpnf  13348  supxrun  13358  prunioo  13521  difreicc  13524  iccsplit  13525  uzsplit  13636  fzm1  13647  expcl2lem  14114  expeq0  14133  expnegz  14137  expaddz  14147  expmulz  14149  sqlecan  14248  facdiv  14326  facwordi  14328  bcpasc  14360  resqrex  15289  absexpz  15344  caubnd  15397  summo  15753  zsum  15754  zprod  15973  rpnnen2lem12  16261  ordvdsmul  16337  nn0rppwr  16598  nn0expgcd  16601  dvdsprime  16724  2mulprm  16730  ge2nprmge4  16738  prmdvdsexpr  16754  prmfac1  16757  pythagtriplem2  16855  4sqlem11  16993  vdwlem6  17024  vdwlem9  17027  vdwlem13  17031  cshwshashlem3  17135  prmlem0  17143  pleval2  18382  pltletr  18388  plelttr  18389  tsrlemax  18631  smndex1mgm  18920  f1omvdco2  19466  psgnunilem2  19513  efgredlemc  19763  frgpuptinv  19789  lt6abl  19913  dmdprdsplit2lem  20065  domneq0  20708  drngmul0orOLD  20761  lvecvs0or  21110  baspartn  22961  0top  22990  indistopon  23008  restntr  23190  cnindis  23300  cmpfi  23416  filconn  23891  ufprim  23917  ufildr  23939  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  ovolicc2lem3  25554  rolle  26028  dvivthlem1  26047  coeaddlem  26288  dgrco  26315  plymul0or  26322  aalioulem3  26376  cxpge0  26725  cxpmul2z  26733  cxpcn3lem  26790  scvxcvx  27029  sqf11  27182  ppiublem1  27246  lgsdir2lem2  27370  lgsqrlem2  27391  2sqnn0  27482  2sqnn  27483  nosepon  27710  nolesgn2ores  27717  nogesgn1ores  27719  nosepne  27725  nolt02o  27740  nosupbnd1lem5  27757  madebdaylemlrcut  27937  madebday  27938  sltlpss  27945  addsproplem2  28003  sleadd1  28022  addsuniflem  28034  mulsproplem9  28150  ssltmul1  28173  ssltmul2  28174  muls0ord  28211  precsexlem9  28239  precsexlem11  28241  recsex  28243  abssnid  28267  sltonold  28283  elnnzs  28387  expsne0  28414  zs12bday  28424  lmieu  28792  upgrpredgv  29156  edglnl  29160  eucrct2eupth  30264  frgrogt3nreg  30416  nvmul0or  30669  hvmul0or  31044  snsssng  32533  disjxpin  32601  expgt0b  32818  subfacp1lem4  35188  satfvsucsuc  35370  satfrnmapom  35375  sat1el2xp  35384  gonarlem  35399  gonar  35400  goalrlem  35401  goalr  35402  fmlasucdisj  35404  satffunlem1lem1  35407  satffunlem2lem1  35409  untsucf  35710  dfon2lem6  35789  broutsideof2  36123  btwnoutside  36126  broutsideof3  36127  outsideoftr  36130  lineunray  36148  lineelsb2  36149  finminlem  36319  nn0prpw  36324  refssfne  36359  meran1  36412  ontgval  36432  ordcmp  36448  bj-sngltag  36984  bj-prmoore  37116  topdifinfindis  37347  icoreclin  37358  rdgssun  37379  finxpsuclem  37398  poimirlem24  37651  poimirlem25  37652  poimirlem29  37656  poimirlem31  37658  mblfinlem2  37665  ovoliunnfl  37669  itg2addnclem  37678  sdclem2  37749  fdc  37752  divrngidl  38035  lkreqN  39171  cvrnbtwn4  39280  4atlem12  39614  elpaddn0  39802  paddasslem17  39838  paddidm  39843  pmapjoin  39854  llnexchb2  39871  dalawlem13  39885  dalawlem14  39886  dochkrshp4  41391  lcfl6  41502  lcmineqlem  42053  primrootspoweq0  42107  aks6d1c1  42117  sticksstones22  42169  aks6d1c6lem3  42173  oexpreposd  42357  expeqidd  42360  sn-sup2  42501  fphpdo  42828  pellfundex  42897  jm2.19lem4  43004  jm2.26a  43012  ordnexbtwnsuc  43280  onov0suclim  43287  oege2  43320  succlg  43341  dflim5  43342  oacl2g  43343  omcl2  43346  omcl3g  43347  naddgeoa  43407  safesnsupfiss  43428  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  relexpmulg  43723  relexp01min  43726  relexpxpmin  43730  relexpaddss  43731  clsk1indlem3  44056  or2expropbi  47046  ich2exprop  47458  poprelb  47511  reuopreuprim  47513  goldbachthlem2  47533  requad01  47608  evenltle  47704  gbowge7  47750  bgoldbtbndlem3  47794  elclnbgrelnbgr  47812  clnbgrel  47815  dfclnbgr6  47842  dfnbgr6  47843  dfsclnbgr6  47844  clnbgrgrim  47902  isubgr3stgrlem4  47936  isubgr3stgrlem7  47939  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  lidldomn1  48147  uzlidlring  48151  prelrrx2b  48635  line2y  48676  itschlc0xyqsol1  48687  itsclc0xyqsolr  48690  inlinecirc02plem  48707