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  1620  psssstr  4050  eqoreldif  4630  opthpr  4795  prel12g  4808  opthprneg  4809  axpr  5364  sotric  5562  sotr2  5566  sotr3  5573  relop  5799  suctr  6405  trsucss  6407  ordelinel  6420  fununi  6567  fnprb  7156  soisoi  7276  ordunisuc2  7788  poxp  8071  soxp  8072  frrlem12  8240  frrlem13  8241  tfrlem11  8320  omordi  8494  om00  8503  odi  8507  omeulem2  8511  oewordi  8520  nnmordi  8560  omsmolem  8586  swoord2  8670  nneneq  9133  dffi3  9337  inf3lem6  9545  cantnfle  9583  cantnflem1  9601  cantnflem2  9602  ttrcltr  9628  r1sdom  9689  r1ord3g  9694  rankxplim3  9796  carddom2  9892  wdomnumr  9977  alephordi  9987  alephdom  9994  cardaleph  10002  djuinf  10102  cfsuc  10170  cfsmolem  10183  sornom  10190  fin23lem25  10237  fin1a2lem11  10323  fin1a2s  10327  zorn2lem7  10415  ttukeylem5  10426  alephval2  10486  fpwwe2lem12  10556  gch2  10589  gchaclem  10592  prub  10908  sqgt0sr  11020  1re  11135  lelttr  11227  ltletr  11229  letr  11231  mul0or  11781  prodgt0  11993  mulge0b  12017  squeeze0  12050  sup2  12103  un0addcl  12461  un0mulcl  12462  nn0sub  12478  elnnz  12525  zindd  12621  rpneg  12967  xrlttri  13081  xrlelttr  13098  xrltletr  13099  xrletr  13100  qextlt  13146  qextle  13147  xmullem2  13208  xlemul1a  13231  xrsupexmnf  13248  xrinfmexpnf  13249  supxrun  13259  prunioo  13425  difreicc  13428  iccsplit  13429  uzsplit  13541  fzm1  13552  expcl2lem  14026  expeq0  14045  expnegz  14049  expaddz  14059  expmulz  14061  sqlecan  14162  facdiv  14240  facwordi  14242  bcpasc  14274  resqrex  15203  absexpz  15258  caubnd  15312  summo  15670  zsum  15671  zprod  15893  rpnnen2lem12  16183  ordvdsmul  16260  nn0rppwr  16521  nn0expgcd  16524  dvdsprime  16647  2mulprm  16653  ge2nprmge4  16662  prmdvdsexpr  16678  prmfac1  16681  pythagtriplem2  16779  4sqlem11  16917  vdwlem6  16948  vdwlem9  16951  vdwlem13  16955  cshwshashlem3  17059  prmlem0  17067  pleval2  18292  pltletr  18298  plelttr  18299  tsrlemax  18543  smndex1mgm  18869  f1omvdco2  19414  psgnunilem2  19461  efgredlemc  19711  frgpuptinv  19737  lt6abl  19861  dmdprdsplit2lem  20013  domneq0  20676  drngmul0orOLD  20729  lvecvs0or  21098  baspartn  22929  0top  22958  indistopon  22976  restntr  23157  cnindis  23267  cmpfi  23383  filconn  23858  ufprim  23884  ufildr  23906  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  ovolicc2lem3  25496  rolle  25967  dvivthlem1  25985  coeaddlem  26224  dgrco  26250  plymul0or  26257  aalioulem3  26311  cxpge0  26660  cxpmul2z  26668  cxpcn3lem  26724  scvxcvx  26963  sqf11  27116  ppiublem1  27179  lgsdir2lem2  27303  lgsqrlem2  27324  2sqnn0  27415  2sqnn  27416  nosepon  27643  nolesgn2ores  27650  nogesgn1ores  27652  nosepne  27658  nolt02o  27673  nosupbnd1lem5  27690  madebdaylemlrcut  27905  madebday  27906  ltslpss  27914  addsproplem2  27976  leadds1  27995  addsuniflem  28007  mulsproplem9  28130  sltmuls1  28153  sltmuls2  28154  muls0ord  28191  precsexlem9  28221  precsexlem11  28223  recsex  28225  abssnid  28249  ltonold  28267  onnolt  28272  eucliddivs  28382  elnnzs  28407  expsne0  28442  bdaypw2n0bndlem  28469  bdayfinbndlem1  28473  z12zsodd  28488  lmieu  28866  upgrpredgv  29222  edglnl  29226  eucrct2eupth  30330  frgrogt3nreg  30482  nvmul0or  30736  hvmul0or  31111  snsssng  32599  disjxpin  32673  expgt0b  32905  axprALT2  35269  subfacp1lem4  35381  satfvsucsuc  35563  satfrnmapom  35568  sat1el2xp  35577  gonarlem  35592  gonar  35593  goalrlem  35594  goalr  35595  fmlasucdisj  35597  satffunlem1lem1  35600  satffunlem2lem1  35602  untsucf  35908  dfon2lem6  35984  broutsideof2  36320  btwnoutside  36323  broutsideof3  36324  outsideoftr  36327  lineunray  36345  lineelsb2  36346  finminlem  36516  nn0prpw  36521  refssfne  36556  meran1  36609  ontgval  36629  ordcmp  36645  axtcond  36676  mh-inf3f1  36739  bj-sngltag  37306  bj-axseprep  37397  bj-prmoore  37443  topdifinfindis  37676  icoreclin  37687  rdgssun  37708  finxpsuclem  37727  poimirlem24  37979  poimirlem25  37980  poimirlem29  37984  poimirlem31  37986  mblfinlem2  37993  ovoliunnfl  37997  itg2addnclem  38006  sdclem2  38077  fdc  38080  divrngidl  38363  lkreqN  39630  cvrnbtwn4  39739  4atlem12  40072  elpaddn0  40260  paddasslem17  40296  paddidm  40301  pmapjoin  40312  llnexchb2  40329  dalawlem13  40343  dalawlem14  40344  dochkrshp4  41849  lcfl6  41960  lcmineqlem  42505  primrootspoweq0  42559  aks6d1c1  42569  sticksstones22  42621  aks6d1c6lem3  42625  oexpreposd  42768  expeqidd  42771  sn-remul0ord  42854  sn-sup2  42950  fphpdo  43263  pellfundex  43332  jm2.19lem4  43438  jm2.26a  43446  ordnexbtwnsuc  43713  onov0suclim  43720  oege2  43753  succlg  43774  dflim5  43775  oacl2g  43776  omcl2  43779  omcl3g  43780  naddgeoa  43840  safesnsupfiss  43860  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  relexpmulg  44155  relexp01min  44158  relexpxpmin  44162  relexpaddss  44163  clsk1indlem3  44488  or2expropbi  47494  ich2exprop  47943  poprelb  47996  reuopreuprim  47998  goldbachthlem2  48021  nprmdvdsfacm1lem2  48096  nprmdvdsfacm1  48099  requad01  48109  evenltle  48205  gbowge7  48251  bgoldbtbndlem3  48295  elclnbgrelnbgr  48313  clnbgrel  48316  dfclnbgr6  48344  dfnbgr6  48345  dfsclnbgr6  48346  upgrimpths  48397  clnbgrgrim  48422  isubgr3stgrlem4  48457  isubgr3stgrlem7  48460  grlimgredgex  48488  gpgedgvtx1  48550  gpgvtxedg0  48551  gpgvtxedg1  48552  lidldomn1  48719  uzlidlring  48723  prelrrx2b  49202  line2y  49243  itschlc0xyqsol1  49254  itsclc0xyqsolr  49257  inlinecirc02plem  49274