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  4084  eqoreldif  4661  opthpr  4827  prel12g  4840  opthprneg  4841  axpr  5397  sotric  5591  sotr2  5595  sotr3  5602  relop  5830  suctr  6439  trsucss  6441  ordelinel  6454  fununi  6610  fnprb  7199  soisoi  7320  ordunisuc2  7837  poxp  8125  soxp  8126  frrlem12  8294  frrlem13  8295  wfrlem14OLD  8334  wfrlem15OLD  8335  tfrlem11  8400  omordi  8576  om00  8585  odi  8589  omeulem2  8593  oewordi  8601  nnmordi  8641  omsmolem  8667  swoord2  8750  nneneq  9218  dffi3  9441  inf3lem6  9645  cantnfle  9683  cantnflem1  9701  cantnflem2  9702  ttrcltr  9728  r1sdom  9786  r1ord3g  9791  rankxplim3  9893  carddom2  9989  wdomnumr  10076  alephordi  10086  alephdom  10093  cardaleph  10101  djuinf  10201  cfsuc  10269  cfsmolem  10282  sornom  10289  fin23lem25  10336  fin1a2lem11  10422  fin1a2s  10426  zorn2lem7  10514  ttukeylem5  10525  alephval2  10584  fpwwe2lem12  10654  gch2  10687  gchaclem  10690  prub  11006  sqgt0sr  11118  1re  11233  lelttr  11323  ltletr  11325  letr  11327  mul0or  11875  prodgt0  12086  mulge0b  12110  squeeze0  12143  sup2  12196  un0addcl  12532  un0mulcl  12533  nn0sub  12549  elnnz  12596  zindd  12692  rpneg  13039  xrlttri  13153  xrlelttr  13170  xrltletr  13171  xrletr  13172  qextlt  13217  qextle  13218  xmullem2  13279  xlemul1a  13302  xrsupexmnf  13319  xrinfmexpnf  13320  supxrun  13330  prunioo  13496  difreicc  13499  iccsplit  13500  uzsplit  13611  fzm1  13622  expcl2lem  14089  expeq0  14108  expnegz  14112  expaddz  14122  expmulz  14124  sqlecan  14225  facdiv  14303  facwordi  14305  bcpasc  14337  resqrex  15267  absexpz  15322  caubnd  15375  summo  15731  zsum  15732  zprod  15951  rpnnen2lem12  16241  ordvdsmul  16317  nn0rppwr  16578  nn0expgcd  16581  dvdsprime  16704  2mulprm  16710  ge2nprmge4  16718  prmdvdsexpr  16734  prmfac1  16737  pythagtriplem2  16835  4sqlem11  16973  vdwlem6  17004  vdwlem9  17007  vdwlem13  17011  cshwshashlem3  17115  prmlem0  17123  pleval2  18345  pltletr  18351  plelttr  18352  tsrlemax  18594  smndex1mgm  18883  f1omvdco2  19427  psgnunilem2  19474  efgredlemc  19724  frgpuptinv  19750  lt6abl  19874  dmdprdsplit2lem  20026  domneq0  20666  drngmul0orOLD  20719  lvecvs0or  21067  baspartn  22890  0top  22919  indistopon  22937  restntr  23118  cnindis  23228  cmpfi  23344  filconn  23819  ufprim  23845  ufildr  23867  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  ovolicc2lem3  25470  rolle  25944  dvivthlem1  25963  coeaddlem  26204  dgrco  26231  plymul0or  26238  aalioulem3  26292  cxpge0  26642  cxpmul2z  26650  cxpcn3lem  26707  scvxcvx  26946  sqf11  27099  ppiublem1  27163  lgsdir2lem2  27287  lgsqrlem2  27308  2sqnn0  27399  2sqnn  27400  nosepon  27627  nolesgn2ores  27634  nogesgn1ores  27636  nosepne  27642  nolt02o  27657  nosupbnd1lem5  27674  madebdaylemlrcut  27854  madebday  27855  sltlpss  27862  addsproplem2  27920  sleadd1  27939  addsuniflem  27951  mulsproplem9  28067  ssltmul1  28090  ssltmul2  28091  muls0ord  28128  precsexlem9  28156  precsexlem11  28158  recsex  28160  abssnid  28184  sltonold  28200  elnnzs  28304  expsne0  28331  zs12bday  28341  lmieu  28709  upgrpredgv  29064  edglnl  29068  eucrct2eupth  30172  frgrogt3nreg  30324  nvmul0or  30577  hvmul0or  30952  snsssng  32441  disjxpin  32515  expgt0b  32741  subfacp1lem4  35151  satfvsucsuc  35333  satfrnmapom  35338  sat1el2xp  35347  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  untsucf  35673  dfon2lem6  35752  broutsideof2  36086  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  lineunray  36111  lineelsb2  36112  finminlem  36282  nn0prpw  36287  refssfne  36322  meran1  36375  ontgval  36395  ordcmp  36411  bj-sngltag  36947  bj-prmoore  37079  topdifinfindis  37310  icoreclin  37321  rdgssun  37342  finxpsuclem  37361  poimirlem24  37614  poimirlem25  37615  poimirlem29  37619  poimirlem31  37621  mblfinlem2  37628  ovoliunnfl  37632  itg2addnclem  37641  sdclem2  37712  fdc  37715  divrngidl  37998  lkreqN  39134  cvrnbtwn4  39243  4atlem12  39577  elpaddn0  39765  paddasslem17  39801  paddidm  39806  pmapjoin  39817  llnexchb2  39834  dalawlem13  39848  dalawlem14  39849  dochkrshp4  41354  lcfl6  41465  lcmineqlem  42011  primrootspoweq0  42065  aks6d1c1  42075  sticksstones22  42127  aks6d1c6lem3  42131  oexpreposd  42318  expeqidd  42321  sn-sup2  42461  fphpdo  42787  pellfundex  42856  jm2.19lem4  42963  jm2.26a  42971  ordnexbtwnsuc  43238  onov0suclim  43245  oege2  43278  succlg  43299  dflim5  43300  oacl2g  43301  omcl2  43304  omcl3g  43305  naddgeoa  43365  safesnsupfiss  43386  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  relexpmulg  43681  relexp01min  43684  relexpxpmin  43688  relexpaddss  43689  clsk1indlem3  44014  or2expropbi  47011  ich2exprop  47433  poprelb  47486  reuopreuprim  47488  goldbachthlem2  47508  requad01  47583  evenltle  47679  gbowge7  47725  bgoldbtbndlem3  47769  elclnbgrelnbgr  47787  clnbgrel  47790  dfclnbgr6  47817  dfnbgr6  47818  dfsclnbgr6  47819  upgrimpths  47870  clnbgrgrim  47895  isubgr3stgrlem4  47929  isubgr3stgrlem7  47932  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  lidldomn1  48154  uzlidlring  48158  prelrrx2b  48642  line2y  48683  itschlc0xyqsol1  48694  itsclc0xyqsolr  48697  inlinecirc02plem  48714