Theorem jaod 858

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  mpjaod  859  orel2  890  pm2.621  898  pm2.63  940  jaao  954  jaodan  957  ecase2dOLD  1030  ecase3d  1033  dedlema  1045  dedlemb  1046  cad0  1620  cad0OLD  1621  psssstr  4107  eqoreldif  4689  opthpr  4853  prel12g  4865  opthprneg  4866  sotric  5617  sotr2  5621  sotr3  5628  relop  5851  suctr  6451  trsucss  6453  ordelinel  6466  fununi  6624  fnprb  7210  soisoi  7325  ordunisuc2  7833  poxp  8114  soxp  8115  frrlem12  8282  frrlem13  8283  wfrlem14OLD  8322  wfrlem15OLD  8323  tfrlem11  8388  omordi  8566  om00  8575  odi  8579  omeulem2  8583  oewordi  8591  nnmordi  8631  omsmolem  8656  swoord2  8735  nneneq  9209  nneneqOLD  9221  dffi3  9426  inf3lem6  9628  cantnfle  9666  cantnflem1  9684  cantnflem2  9685  ttrcltr  9711  r1sdom  9769  r1ord3g  9774  rankxplim3  9876  carddom2  9972  wdomnumr  10059  alephordi  10069  alephdom  10076  cardaleph  10084  djuinf  10183  cfsuc  10252  cfsmolem  10265  sornom  10272  fin23lem25  10319  fin1a2lem11  10405  fin1a2s  10409  zorn2lem7  10497  ttukeylem5  10508  alephval2  10567  fpwwe2lem12  10637  gch2  10670  gchaclem  10673  prub  10989  sqgt0sr  11101  1re  11214  lelttr  11304  ltletr  11306  letr  11308  mul0or  11854  prodgt0  12061  mulge0b  12084  squeeze0  12117  sup2  12170  un0addcl  12505  un0mulcl  12506  nn0sub  12522  elnnz  12568  zindd  12663  rpneg  13006  xrlttri  13118  xrlelttr  13135  xrltletr  13136  xrletr  13137  qextlt  13182  qextle  13183  xmullem2  13244  xlemul1a  13267  xrsupexmnf  13284  xrinfmexpnf  13285  supxrun  13295  prunioo  13458  difreicc  13461  iccsplit  13462  uzsplit  13573  fzm1  13581  expcl2lem  14039  expeq0  14058  expnegz  14062  expaddz  14072  expmulz  14074  sqlecan  14173  facdiv  14247  facwordi  14249  bcpasc  14281  resqrex  15197  absexpz  15252  caubnd  15305  summo  15663  zsum  15664  zprod  15881  rpnnen2lem12  16168  ordvdsmul  16243  dvdsprime  16624  2mulprm  16630  ge2nprmge4  16638  prmdvdsexpr  16654  prmfac1  16658  pythagtriplem2  16750  4sqlem11  16888  vdwlem6  16919  vdwlem9  16922  vdwlem13  16926  cshwshashlem3  17031  prmlem0  17039  pleval2  18290  pltletr  18296  plelttr  18297  tsrlemax  18539  smndex1mgm  18788  f1omvdco2  19316  psgnunilem2  19363  efgredlemc  19613  frgpuptinv  19639  lt6abl  19763  dmdprdsplit2lem  19915  drngmul0or  20386  lvecvs0or  20721  domneq0  20913  baspartn  22457  0top  22486  indistopon  22504  restntr  22686  cnindis  22796  cmpfi  22912  filconn  23387  ufprim  23413  ufildr  23435  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  ovolicc2lem3  25036  rolle  25507  dvivthlem1  25525  coeaddlem  25763  dgrco  25789  plymul0or  25794  aalioulem3  25847  cxpge0  26191  cxpmul2z  26199  cxpcn3lem  26255  scvxcvx  26490  sqf11  26643  ppiublem1  26705  lgsdir2lem2  26829  lgsqrlem2  26850  2sqnn0  26941  2sqnn  26942  nosepon  27168  nolesgn2ores  27175  nogesgn1ores  27177  nosepne  27183  nolt02o  27198  nosupbnd1lem5  27215  madebdaylemlrcut  27393  madebday  27394  sltlpss  27401  addsproplem2  27454  sleadd1  27472  addsuniflem  27484  mulsproplem9  27580  ssltmul1  27602  ssltmul2  27603  precsexlem9  27661  precsexlem11  27663  recsex  27665  lmieu  28035  upgrpredgv  28399  edglnl  28403  eucrct2eupth  29498  frgrogt3nreg  29650  nvmul0or  29903  hvmul0or  30278  snsssng  31752  disjxpin  31819  subfacp1lem4  34174  satfvsucsuc  34356  satfrnmapom  34361  sat1el2xp  34370  gonarlem  34385  gonar  34386  goalrlem  34387  goalr  34388  fmlasucdisj  34390  satffunlem1lem1  34393  satffunlem2lem1  34395  untsucf  34679  dfon2lem6  34760  broutsideof2  35094  btwnoutside  35097  broutsideof3  35098  outsideoftr  35101  lineunray  35119  lineelsb2  35120  finminlem  35203  nn0prpw  35208  refssfne  35243  meran1  35296  ontgval  35316  ordcmp  35332  bj-sngltag  35864  bj-prmoore  35996  topdifinfindis  36227  icoreclin  36238  rdgssun  36259  finxpsuclem  36278  poimirlem24  36512  poimirlem25  36513  poimirlem29  36517  poimirlem31  36519  mblfinlem2  36526  ovoliunnfl  36530  itg2addnclem  36539  sdclem2  36610  fdc  36613  divrngidl  36896  lkreqN  38040  cvrnbtwn4  38149  4atlem12  38483  elpaddn0  38671  paddasslem17  38707  paddidm  38712  pmapjoin  38723  llnexchb2  38740  dalawlem13  38754  dalawlem14  38755  dochkrshp4  40260  lcfl6  40371  lcmineqlem  40917  sticksstones22  40984  oexpreposd  41212  nn0rppwr  41224  nn0expgcd  41226  sn-sup2  41342  fphpdo  41555  pellfundex  41624  jm2.19lem4  41731  jm2.26a  41739  ordnexbtwnsuc  42017  onov0suclim  42024  oege2  42057  succlg  42078  dflim5  42079  oacl2g  42080  omcl2  42083  omcl3g  42084  naddgeoa  42145  safesnsupfiss  42166  fzunt  42206  fzuntd  42207  fzunt1d  42208  fzuntgd  42209  relexpmulg  42461  relexp01min  42464  relexpxpmin  42468  relexpaddss  42469  clsk1indlem3  42794  or2expropbi  45744  ich2exprop  46139  poprelb  46192  reuopreuprim  46194  goldbachthlem2  46214  requad01  46289  evenltle  46385  gbowge7  46431  bgoldbtbndlem3  46475  lidldomn1  46823  uzlidlring  46827  prelrrx2b  47400  line2y  47441  itschlc0xyqsol1  47452  itsclc0xyqsolr  47455  inlinecirc02plem  47472