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  4075  eqoreldif  4652  opthpr  4818  prel12g  4831  opthprneg  4832  axpr  5385  sotric  5579  sotr2  5583  sotr3  5590  relop  5817  suctr  6423  trsucss  6425  ordelinel  6438  fununi  6594  fnprb  7185  soisoi  7306  ordunisuc2  7823  poxp  8110  soxp  8111  frrlem12  8279  frrlem13  8280  tfrlem11  8359  omordi  8533  om00  8542  odi  8546  omeulem2  8550  oewordi  8558  nnmordi  8598  omsmolem  8624  swoord2  8707  nneneq  9176  dffi3  9389  inf3lem6  9593  cantnfle  9631  cantnflem1  9649  cantnflem2  9650  ttrcltr  9676  r1sdom  9734  r1ord3g  9739  rankxplim3  9841  carddom2  9937  wdomnumr  10024  alephordi  10034  alephdom  10041  cardaleph  10049  djuinf  10149  cfsuc  10217  cfsmolem  10230  sornom  10237  fin23lem25  10284  fin1a2lem11  10370  fin1a2s  10374  zorn2lem7  10462  ttukeylem5  10473  alephval2  10532  fpwwe2lem12  10602  gch2  10635  gchaclem  10638  prub  10954  sqgt0sr  11066  1re  11181  lelttr  11271  ltletr  11273  letr  11275  mul0or  11825  prodgt0  12036  mulge0b  12060  squeeze0  12093  sup2  12146  un0addcl  12482  un0mulcl  12483  nn0sub  12499  elnnz  12546  zindd  12642  rpneg  12992  xrlttri  13106  xrlelttr  13123  xrltletr  13124  xrletr  13125  qextlt  13170  qextle  13171  xmullem2  13232  xlemul1a  13255  xrsupexmnf  13272  xrinfmexpnf  13273  supxrun  13283  prunioo  13449  difreicc  13452  iccsplit  13453  uzsplit  13564  fzm1  13575  expcl2lem  14045  expeq0  14064  expnegz  14068  expaddz  14078  expmulz  14080  sqlecan  14181  facdiv  14259  facwordi  14261  bcpasc  14293  resqrex  15223  absexpz  15278  caubnd  15332  summo  15690  zsum  15691  zprod  15910  rpnnen2lem12  16200  ordvdsmul  16277  nn0rppwr  16538  nn0expgcd  16541  dvdsprime  16664  2mulprm  16670  ge2nprmge4  16678  prmdvdsexpr  16694  prmfac1  16697  pythagtriplem2  16795  4sqlem11  16933  vdwlem6  16964  vdwlem9  16967  vdwlem13  16971  cshwshashlem3  17075  prmlem0  17083  pleval2  18303  pltletr  18309  plelttr  18310  tsrlemax  18552  smndex1mgm  18841  f1omvdco2  19385  psgnunilem2  19432  efgredlemc  19682  frgpuptinv  19708  lt6abl  19832  dmdprdsplit2lem  19984  domneq0  20624  drngmul0orOLD  20677  lvecvs0or  21025  baspartn  22848  0top  22877  indistopon  22895  restntr  23076  cnindis  23186  cmpfi  23302  filconn  23777  ufprim  23803  ufildr  23825  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  ovolicc2lem3  25427  rolle  25901  dvivthlem1  25920  coeaddlem  26161  dgrco  26188  plymul0or  26195  aalioulem3  26249  cxpge0  26599  cxpmul2z  26607  cxpcn3lem  26664  scvxcvx  26903  sqf11  27056  ppiublem1  27120  lgsdir2lem2  27244  lgsqrlem2  27265  2sqnn0  27356  2sqnn  27357  nosepon  27584  nolesgn2ores  27591  nogesgn1ores  27593  nosepne  27599  nolt02o  27614  nosupbnd1lem5  27631  madebdaylemlrcut  27817  madebday  27818  sltlpss  27826  addsproplem2  27884  sleadd1  27903  addsuniflem  27915  mulsproplem9  28034  ssltmul1  28057  ssltmul2  28058  muls0ord  28095  precsexlem9  28124  precsexlem11  28126  recsex  28128  abssnid  28152  sltonold  28169  onnolt  28174  eucliddivs  28272  elnnzs  28296  expsne0  28328  zs12bday  28350  lmieu  28718  upgrpredgv  29073  edglnl  29077  eucrct2eupth  30181  frgrogt3nreg  30333  nvmul0or  30586  hvmul0or  30961  snsssng  32450  disjxpin  32524  expgt0b  32748  subfacp1lem4  35177  satfvsucsuc  35359  satfrnmapom  35364  sat1el2xp  35373  gonarlem  35388  gonar  35389  goalrlem  35390  goalr  35391  fmlasucdisj  35393  satffunlem1lem1  35396  satffunlem2lem1  35398  untsucf  35704  dfon2lem6  35783  broutsideof2  36117  btwnoutside  36120  broutsideof3  36121  outsideoftr  36124  lineunray  36142  lineelsb2  36143  finminlem  36313  nn0prpw  36318  refssfne  36353  meran1  36406  ontgval  36426  ordcmp  36442  bj-sngltag  36978  bj-prmoore  37110  topdifinfindis  37341  icoreclin  37352  rdgssun  37373  finxpsuclem  37392  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  mblfinlem2  37659  ovoliunnfl  37663  itg2addnclem  37672  sdclem2  37743  fdc  37746  divrngidl  38029  lkreqN  39170  cvrnbtwn4  39279  4atlem12  39613  elpaddn0  39801  paddasslem17  39837  paddidm  39842  pmapjoin  39853  llnexchb2  39870  dalawlem13  39884  dalawlem14  39885  dochkrshp4  41390  lcfl6  41501  lcmineqlem  42047  primrootspoweq0  42101  aks6d1c1  42111  sticksstones22  42163  aks6d1c6lem3  42167  oexpreposd  42317  expeqidd  42320  sn-remul0ord  42403  sn-sup2  42486  fphpdo  42812  pellfundex  42881  jm2.19lem4  42988  jm2.26a  42996  ordnexbtwnsuc  43263  onov0suclim  43270  oege2  43303  succlg  43324  dflim5  43325  oacl2g  43326  omcl2  43329  omcl3g  43330  naddgeoa  43390  safesnsupfiss  43411  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  relexpmulg  43706  relexp01min  43709  relexpxpmin  43713  relexpaddss  43714  clsk1indlem3  44039  or2expropbi  47039  ich2exprop  47476  poprelb  47529  reuopreuprim  47531  goldbachthlem2  47551  requad01  47626  evenltle  47722  gbowge7  47768  bgoldbtbndlem3  47812  elclnbgrelnbgr  47830  clnbgrel  47833  dfclnbgr6  47860  dfnbgr6  47861  dfsclnbgr6  47862  upgrimpths  47913  clnbgrgrim  47938  isubgr3stgrlem4  47972  isubgr3stgrlem7  47975  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  lidldomn1  48223  uzlidlring  48227  prelrrx2b  48707  line2y  48748  itschlc0xyqsol1  48759  itsclc0xyqsolr  48762  inlinecirc02plem  48779