Theorem jaod 859

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

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  mpjaod  860  orel2  890  pm2.621  898  pm2.63  942  jaao  956  jaodan  959  ecase3d  1034  dedlema  1045  dedlemb  1046  cad0  1618  psssstr  4072  eqoreldif  4649  opthpr  4815  prel12g  4828  opthprneg  4829  axpr  5382  sotric  5576  sotr2  5580  sotr3  5587  relop  5814  suctr  6420  trsucss  6422  ordelinel  6435  fununi  6591  fnprb  7182  soisoi  7303  ordunisuc2  7820  poxp  8107  soxp  8108  frrlem12  8276  frrlem13  8277  tfrlem11  8356  omordi  8530  om00  8539  odi  8543  omeulem2  8547  oewordi  8555  nnmordi  8595  omsmolem  8621  swoord2  8704  nneneq  9170  dffi3  9382  inf3lem6  9586  cantnfle  9624  cantnflem1  9642  cantnflem2  9643  ttrcltr  9669  r1sdom  9727  r1ord3g  9732  rankxplim3  9834  carddom2  9930  wdomnumr  10017  alephordi  10027  alephdom  10034  cardaleph  10042  djuinf  10142  cfsuc  10210  cfsmolem  10223  sornom  10230  fin23lem25  10277  fin1a2lem11  10363  fin1a2s  10367  zorn2lem7  10455  ttukeylem5  10466  alephval2  10525  fpwwe2lem12  10595  gch2  10628  gchaclem  10631  prub  10947  sqgt0sr  11059  1re  11174  lelttr  11264  ltletr  11266  letr  11268  mul0or  11818  prodgt0  12029  mulge0b  12053  squeeze0  12086  sup2  12139  un0addcl  12475  un0mulcl  12476  nn0sub  12492  elnnz  12539  zindd  12635  rpneg  12985  xrlttri  13099  xrlelttr  13116  xrltletr  13117  xrletr  13118  qextlt  13163  qextle  13164  xmullem2  13225  xlemul1a  13248  xrsupexmnf  13265  xrinfmexpnf  13266  supxrun  13276  prunioo  13442  difreicc  13445  iccsplit  13446  uzsplit  13557  fzm1  13568  expcl2lem  14038  expeq0  14057  expnegz  14061  expaddz  14071  expmulz  14073  sqlecan  14174  facdiv  14252  facwordi  14254  bcpasc  14286  resqrex  15216  absexpz  15271  caubnd  15325  summo  15683  zsum  15684  zprod  15903  rpnnen2lem12  16193  ordvdsmul  16270  nn0rppwr  16531  nn0expgcd  16534  dvdsprime  16657  2mulprm  16663  ge2nprmge4  16671  prmdvdsexpr  16687  prmfac1  16690  pythagtriplem2  16788  4sqlem11  16926  vdwlem6  16957  vdwlem9  16960  vdwlem13  16964  cshwshashlem3  17068  prmlem0  17076  pleval2  18296  pltletr  18302  plelttr  18303  tsrlemax  18545  smndex1mgm  18834  f1omvdco2  19378  psgnunilem2  19425  efgredlemc  19675  frgpuptinv  19701  lt6abl  19825  dmdprdsplit2lem  19977  domneq0  20617  drngmul0orOLD  20670  lvecvs0or  21018  baspartn  22841  0top  22870  indistopon  22888  restntr  23069  cnindis  23179  cmpfi  23295  filconn  23770  ufprim  23796  ufildr  23818  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  ovolicc2lem3  25420  rolle  25894  dvivthlem1  25913  coeaddlem  26154  dgrco  26181  plymul0or  26188  aalioulem3  26242  cxpge0  26592  cxpmul2z  26600  cxpcn3lem  26657  scvxcvx  26896  sqf11  27049  ppiublem1  27113  lgsdir2lem2  27237  lgsqrlem2  27258  2sqnn0  27349  2sqnn  27350  nosepon  27577  nolesgn2ores  27584  nogesgn1ores  27586  nosepne  27592  nolt02o  27607  nosupbnd1lem5  27624  madebdaylemlrcut  27810  madebday  27811  sltlpss  27819  addsproplem2  27877  sleadd1  27896  addsuniflem  27908  mulsproplem9  28027  ssltmul1  28050  ssltmul2  28051  muls0ord  28088  precsexlem9  28117  precsexlem11  28119  recsex  28121  abssnid  28145  sltonold  28162  onnolt  28167  eucliddivs  28265  elnnzs  28289  expsne0  28321  zs12bday  28343  lmieu  28711  upgrpredgv  29066  edglnl  29070  eucrct2eupth  30174  frgrogt3nreg  30326  nvmul0or  30579  hvmul0or  30954  snsssng  32443  disjxpin  32517  expgt0b  32741  subfacp1lem4  35170  satfvsucsuc  35352  satfrnmapom  35357  sat1el2xp  35366  gonarlem  35381  gonar  35382  goalrlem  35383  goalr  35384  fmlasucdisj  35386  satffunlem1lem1  35389  satffunlem2lem1  35391  untsucf  35697  dfon2lem6  35776  broutsideof2  36110  btwnoutside  36113  broutsideof3  36114  outsideoftr  36117  lineunray  36135  lineelsb2  36136  finminlem  36306  nn0prpw  36311  refssfne  36346  meran1  36399  ontgval  36419  ordcmp  36435  bj-sngltag  36971  bj-prmoore  37103  topdifinfindis  37334  icoreclin  37345  rdgssun  37366  finxpsuclem  37385  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  mblfinlem2  37652  ovoliunnfl  37656  itg2addnclem  37665  sdclem2  37736  fdc  37739  divrngidl  38022  lkreqN  39163  cvrnbtwn4  39272  4atlem12  39606  elpaddn0  39794  paddasslem17  39830  paddidm  39835  pmapjoin  39846  llnexchb2  39863  dalawlem13  39877  dalawlem14  39878  dochkrshp4  41383  lcfl6  41494  lcmineqlem  42040  primrootspoweq0  42094  aks6d1c1  42104  sticksstones22  42156  aks6d1c6lem3  42160  oexpreposd  42310  expeqidd  42313  sn-remul0ord  42396  sn-sup2  42479  fphpdo  42805  pellfundex  42874  jm2.19lem4  42981  jm2.26a  42989  ordnexbtwnsuc  43256  onov0suclim  43263  oege2  43296  succlg  43317  dflim5  43318  oacl2g  43319  omcl2  43322  omcl3g  43323  naddgeoa  43383  safesnsupfiss  43404  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  relexpmulg  43699  relexp01min  43702  relexpxpmin  43706  relexpaddss  43707  clsk1indlem3  44032  or2expropbi  47035  ich2exprop  47472  poprelb  47525  reuopreuprim  47527  goldbachthlem2  47547  requad01  47622  evenltle  47718  gbowge7  47764  bgoldbtbndlem3  47808  elclnbgrelnbgr  47826  clnbgrel  47829  dfclnbgr6  47856  dfnbgr6  47857  dfsclnbgr6  47858  upgrimpths  47909  clnbgrgrim  47934  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  lidldomn1  48219  uzlidlring  48223  prelrrx2b  48703  line2y  48744  itschlc0xyqsol1  48755  itsclc0xyqsolr  48758  inlinecirc02plem  48775