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  4049  eqoreldif  4629  opthpr  4794  prel12g  4807  opthprneg  4808  axpr  5369  sotric  5569  sotr2  5573  sotr3  5580  relop  5805  suctr  6411  trsucss  6413  ordelinel  6426  fununi  6573  fnprb  7163  soisoi  7283  ordunisuc2  7795  poxp  8078  soxp  8079  frrlem12  8247  frrlem13  8248  tfrlem11  8327  omordi  8501  om00  8510  odi  8514  omeulem2  8518  oewordi  8527  nnmordi  8567  omsmolem  8593  swoord2  8677  nneneq  9140  dffi3  9344  inf3lem6  9554  cantnfle  9592  cantnflem1  9610  cantnflem2  9611  ttrcltr  9637  r1sdom  9698  r1ord3g  9703  rankxplim3  9805  carddom2  9901  wdomnumr  9986  alephordi  9996  alephdom  10003  cardaleph  10011  djuinf  10111  cfsuc  10179  cfsmolem  10192  sornom  10199  fin23lem25  10246  fin1a2lem11  10332  fin1a2s  10336  zorn2lem7  10424  ttukeylem5  10435  alephval2  10495  fpwwe2lem12  10565  gch2  10598  gchaclem  10601  prub  10917  sqgt0sr  11029  1re  11144  lelttr  11236  ltletr  11238  letr  11240  mul0or  11790  prodgt0  12002  mulge0b  12026  squeeze0  12059  sup2  12112  un0addcl  12470  un0mulcl  12471  nn0sub  12487  elnnz  12534  zindd  12630  rpneg  12976  xrlttri  13090  xrlelttr  13107  xrltletr  13108  xrletr  13109  qextlt  13155  qextle  13156  xmullem2  13217  xlemul1a  13240  xrsupexmnf  13257  xrinfmexpnf  13258  supxrun  13268  prunioo  13434  difreicc  13437  iccsplit  13438  uzsplit  13550  fzm1  13561  expcl2lem  14035  expeq0  14054  expnegz  14058  expaddz  14068  expmulz  14070  sqlecan  14171  facdiv  14249  facwordi  14251  bcpasc  14283  resqrex  15212  absexpz  15267  caubnd  15321  summo  15679  zsum  15680  zprod  15902  rpnnen2lem12  16192  ordvdsmul  16269  nn0rppwr  16530  nn0expgcd  16533  dvdsprime  16656  2mulprm  16662  ge2nprmge4  16671  prmdvdsexpr  16687  prmfac1  16690  pythagtriplem2  16788  4sqlem11  16926  vdwlem6  16957  vdwlem9  16960  vdwlem13  16964  cshwshashlem3  17068  prmlem0  17076  pleval2  18301  pltletr  18307  plelttr  18308  tsrlemax  18552  smndex1mgm  18878  f1omvdco2  19423  psgnunilem2  19470  efgredlemc  19720  frgpuptinv  19746  lt6abl  19870  dmdprdsplit2lem  20022  domneq0  20685  drngmul0orOLD  20738  lvecvs0or  21106  baspartn  22919  0top  22948  indistopon  22966  restntr  23147  cnindis  23257  cmpfi  23373  filconn  23848  ufprim  23874  ufildr  23896  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  ovolicc2lem3  25486  rolle  25957  dvivthlem1  25975  coeaddlem  26214  dgrco  26240  plymul0or  26247  aalioulem3  26300  cxpge0  26647  cxpmul2z  26655  cxpcn3lem  26711  scvxcvx  26949  sqf11  27102  ppiublem1  27165  lgsdir2lem2  27289  lgsqrlem2  27310  2sqnn0  27401  2sqnn  27402  nosepon  27629  nolesgn2ores  27636  nogesgn1ores  27638  nosepne  27644  nolt02o  27659  nosupbnd1lem5  27676  madebdaylemlrcut  27891  madebday  27892  ltslpss  27900  addsproplem2  27962  leadds1  27981  addsuniflem  27993  mulsproplem9  28116  sltmuls1  28139  sltmuls2  28140  muls0ord  28177  precsexlem9  28207  precsexlem11  28209  recsex  28211  abssnid  28235  ltonold  28253  onnolt  28258  eucliddivs  28368  elnnzs  28393  expsne0  28428  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  z12zsodd  28474  lmieu  28852  upgrpredgv  29208  edglnl  29212  eucrct2eupth  30315  frgrogt3nreg  30467  nvmul0or  30721  hvmul0or  31096  snsssng  32584  disjxpin  32658  expgt0b  32890  axprALT2  35253  subfacp1lem4  35365  satfvsucsuc  35547  satfrnmapom  35552  sat1el2xp  35561  gonarlem  35576  gonar  35577  goalrlem  35578  goalr  35579  fmlasucdisj  35581  satffunlem1lem1  35584  satffunlem2lem1  35586  untsucf  35892  dfon2lem6  35968  broutsideof2  36304  btwnoutside  36307  broutsideof3  36308  outsideoftr  36311  lineunray  36329  lineelsb2  36330  finminlem  36500  nn0prpw  36505  refssfne  36540  meran1  36593  ontgval  36613  ordcmp  36629  axtcond  36660  mh-inf3f1  36723  bj-sngltag  37290  bj-axseprep  37381  bj-prmoore  37427  topdifinfindis  37662  icoreclin  37673  rdgssun  37694  finxpsuclem  37713  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  mblfinlem2  37979  ovoliunnfl  37983  itg2addnclem  37992  sdclem2  38063  fdc  38066  divrngidl  38349  lkreqN  39616  cvrnbtwn4  39725  4atlem12  40058  elpaddn0  40246  paddasslem17  40282  paddidm  40287  pmapjoin  40298  llnexchb2  40315  dalawlem13  40329  dalawlem14  40330  dochkrshp4  41835  lcfl6  41946  lcmineqlem  42491  primrootspoweq0  42545  aks6d1c1  42555  sticksstones22  42607  aks6d1c6lem3  42611  oexpreposd  42754  expeqidd  42757  sn-remul0ord  42840  sn-sup2  42936  fphpdo  43245  pellfundex  43314  jm2.19lem4  43420  jm2.26a  43428  ordnexbtwnsuc  43695  onov0suclim  43702  oege2  43735  succlg  43756  dflim5  43757  oacl2g  43758  omcl2  43761  omcl3g  43762  naddgeoa  43822  safesnsupfiss  43842  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  relexpmulg  44137  relexp01min  44140  relexpxpmin  44144  relexpaddss  44145  clsk1indlem3  44470  or2expropbi  47482  ich2exprop  47931  poprelb  47984  reuopreuprim  47986  goldbachthlem2  48009  nprmdvdsfacm1lem2  48084  nprmdvdsfacm1  48087  requad01  48097  evenltle  48193  gbowge7  48239  bgoldbtbndlem3  48283  elclnbgrelnbgr  48301  clnbgrel  48304  dfclnbgr6  48332  dfnbgr6  48333  dfsclnbgr6  48334  upgrimpths  48385  clnbgrgrim  48410  isubgr3stgrlem4  48445  isubgr3stgrlem7  48448  grlimgredgex  48476  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  lidldomn1  48707  uzlidlring  48711  prelrrx2b  49190  line2y  49231  itschlc0xyqsol1  49242  itsclc0xyqsolr  49245  inlinecirc02plem  49262