Theorem jaod 870

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  mpjaod  871  orel2  901  pm2.621  909  pm2.63  953  jaao  967  jaodan  970  ecase3d  1045  dedlema  1056  dedlemb  1057  cad0  1637  psssstr  4061  eqoreldif  4641  opthpr  4806  prel12g  4819  opthprneg  4820  axpr  5381  sotric  5581  sotr2  5585  sotr3  5592  relop  5818  suctr  6428  trsucss  6430  ordelinel  6443  fununi  6590  fnprb  7186  soisoi  7306  ordunisuc2  7818  poxp  8101  soxp  8102  frrlem12  8271  frrlem13  8272  tfrlem11  8352  omordi  8528  om00  8537  odi  8541  omeulem2  8545  oewordi  8554  nnmordi  8594  omsmolem  8620  swoord2  8705  nneneq  9167  dffi3  9370  inf3lem6  9581  cantnfle  9619  cantnflem1  9637  cantnflem2  9638  ttrcltr  9664  r1sdom  9725  r1ord3g  9730  rankxplim3  9832  carddom2  9928  wdomnumr  10013  alephordi  10023  alephdom  10030  cardaleph  10038  djuinf  10138  cfsuc  10207  cfsmolem  10220  sornom  10227  fin23lem25  10274  fin1a2lem11  10360  fin1a2s  10364  zorn2lem7  10452  ttukeylem5  10463  alephval2  10523  fpwwe2lem12  10593  gch2  10626  gchaclem  10629  prub  10945  sqgt0sr  11057  1re  11174  lelttr  11266  ltletr  11268  letr  11270  mul0or  11820  prodgt0  12031  mulge0b  12055  squeeze0  12088  sup2  12141  un0addcl  12507  un0mulcl  12508  nn0sub  12524  elnnz  12571  zindd  12667  rpneg  13020  xrlttri  13134  xrlelttr  13151  xrltletr  13152  xrletr  13153  qextlt  13199  qextle  13200  xmullem2  13261  xlemul1a  13284  xrsupexmnf  13301  xrinfmexpnf  13302  supxrun  13312  prunioo  13478  difreicc  13481  iccsplit  13482  uzsplit  13594  fzm1  13605  expcl2lem  14079  expeq0  14098  expnegz  14102  expaddz  14112  expmulz  14114  sqlecan  14215  facdiv  14293  facwordi  14295  bcpasc  14327  resqrex  15267  absexpz  15322  caubnd  15376  summo  15734  zsum  15735  zprod  15957  rpnnen2lem12  16247  ordvdsmul  16324  nn0rppwr  16585  nn0expgcd  16588  dvdsprime  16711  2mulprm  16717  ge2nprmge4  16726  prmdvdsexpr  16742  prmfac1  16745  pythagtriplem2  16843  4sqlem11  16981  vdwlem6  17012  vdwlem9  17015  vdwlem13  17019  cshwshashlem3  17123  prmlem0  17131  pleval2  18357  pltletr  18363  plelttr  18364  tsrlemax  18608  smndex1mgm  18934  f1omvdco2  19478  psgnunilem2  19525  efgredlemc  19775  frgpuptinv  19801  lt6abl  19925  dmdprdsplit2lem  20077  domneq0  20744  drngmul0orOLD  20797  lvecvs0or  21165  baspartn  23001  0top  23030  indistopon  23048  restntr  23229  cnindis  23339  cmpfi  23455  filconn  23930  ufprim  23956  ufildr  23978  alexsubALTlem2  24095  alexsubALTlem3  24096  alexsubALTlem4  24097  ovolicc2lem3  25568  rolle  26039  dvivthlem1  26057  coeaddlem  26296  dgrco  26322  plymul0or  26329  aalioulem3  26385  cxpge0  26735  cxpmul2z  26743  cxpcn3lem  26799  scvxcvx  27037  sqf11  27190  ppiublem1  27253  lgsdir2lem2  27377  lgsqrlem2  27398  2sqnn0  27489  2sqnn  27490  nosepon  27716  nolesgn2ores  27723  nogesgn1ores  27725  nosepne  27731  nolt02o  27746  nosupbnd1lem5  27763  madebdaylemlrcut  27979  madebday  27980  ltslpss  27988  addsproplem2  28050  leadds1  28069  addsuniflem  28081  mulsproplem9  28204  sltmuls1  28227  sltmuls2  28228  muls0ord  28265  precsexlem9  28295  precsexlem11  28297  recsex  28299  abssnid  28323  ltonold  28341  onnolt  28346  eucliddivs  28456  elnnzs  28481  expsne0  28516  bdaypw2n0bndlem  28543  bdayfinbndlem1  28547  z12zsodd  28562  lmieu  28940  upgrpredgv  29296  edglnl  29300  eucrct2eupth  30403  frgrogt3nreg  30555  nvmul0or  30809  hvmul0or  31184  snsssng  32672  disjxpin  32747  expgt0b  32979  axprALT2  35365  subfacp1lem4  35493  satfvsucsuc  35675  satfrnmapom  35680  sat1el2xp  35689  gonarlem  35704  gonar  35705  goalrlem  35706  goalr  35707  fmlasucdisj  35709  satffunlem1lem1  35712  satffunlem2lem1  35714  untsucf  36020  dfon2lem6  36096  broutsideof2  36432  btwnoutside  36435  broutsideof3  36436  outsideoftr  36439  lineunray  36457  lineelsb2  36458  finminlem  36638  nn0prpw  36643  refssfne  36678  meran1  36731  ontgval  36751  ordcmp  36767  axtcond  36798  mh-inf3f1  36861  bj-sngltag  37428  bj-axseprep  37519  bj-prmoore  37565  topdifinfindis  37800  icoreclin  37811  rdgssun  37832  finxpsuclem  37851  poimirlem24  38103  poimirlem25  38104  poimirlem29  38108  poimirlem31  38110  mblfinlem2  38117  ovoliunnfl  38121  itg2addnclem  38130  sdclem2  38201  fdc  38204  divrngidl  38487  lkreqN  39754  cvrnbtwn4  39863  4atlem12  40196  elpaddn0  40384  paddasslem17  40420  paddidm  40425  pmapjoin  40436  llnexchb2  40453  dalawlem13  40467  dalawlem14  40468  dochkrshp4  41973  lcfl6  42084  lcmineqlem  42629  primrootspoweq0  42683  aks6d1c1  42693  sticksstones22  42745  aks6d1c6lem3  42749  oexpreposd  42891  expeqidd  42894  sn-remul0ord  42977  sn-sup2  43073  fphpdo  43354  pellfundex  43423  jm2.19lem4  43529  jm2.26a  43537  ordnexbtwnsuc  43804  onov0suclim  43811  oege2  43844  succlg  43865  dflim5  43866  oacl2g  43867  omcl2  43870  omcl3g  43871  naddgeoa  43931  safesnsupfiss  43951  fzunt  43991  fzuntd  43992  fzunt1d  43993  fzuntgd  43994  relexpmulg  44246  relexp01min  44249  relexpxpmin  44253  relexpaddss  44254  clsk1indlem3  44579  or2expropbi  47588  ich2exprop  48037  poprelb  48090  reuopreuprim  48092  goldbachthlem2  48115  nprmdvdsfacm1lem2  48190  nprmdvdsfacm1  48193  requad01  48203  evenltle  48299  gbowge7  48345  bgoldbtbndlem3  48389  elclnbgrelnbgr  48407  clnbgrel  48410  dfclnbgr6  48438  dfnbgr6  48439  dfsclnbgr6  48440  upgrimpths  48491  clnbgrgrim  48516  isubgr3stgrlem4  48551  isubgr3stgrlem7  48554  grlimgredgex  48582  gpgedgvtx1  48644  gpgvtxedg0  48645  gpgvtxedg1  48646  lidldomn1  48813  uzlidlring  48817  prelrrx2b  49296  line2y  49337  itschlc0xyqsol1  49348  itsclc0xyqsolr  49351  inlinecirc02plem  49368