Theorem jaod 856

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

Syntax hints:   → wi 4   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  mpjaod  857  orel2  888  pm2.621  896  pm2.63  938  jaao  952  jaodan  955  ecase2d  1027  ecase3d  1030  dedlema  1041  dedlemb  1042  cad0  1619  psssstr  4034  eqoreldif  4582  opthpr  4742  prel12g  4754  opthprneg  4755  sotric  5465  sotr2  5469  relop  5685  suctr  6242  trsucss  6244  ordelinel  6257  fununi  6399  fnprb  6948  soisoi  7060  ordunisuc2  7539  poxp  7805  soxp  7806  wfrlem14  7951  wfrlem15  7952  tfrlem11  8007  omordi  8175  om00  8184  odi  8188  omeulem2  8192  oewordi  8200  nnmordi  8240  omsmolem  8263  swoord2  8304  nneneq  8684  dffi3  8879  inf3lem6  9080  cantnfle  9118  cantnflem1  9136  cantnflem2  9137  r1sdom  9187  r1ord3g  9192  rankxplim3  9294  carddom2  9390  wdomnumr  9475  alephordi  9485  alephdom  9492  cardaleph  9500  djuinf  9599  cfsuc  9668  cfsmolem  9681  sornom  9688  fin23lem25  9735  fin1a2lem11  9821  fin1a2s  9825  zorn2lem7  9913  ttukeylem5  9924  alephval2  9983  fpwwe2lem13  10053  gch2  10086  gchaclem  10089  prub  10405  sqgt0sr  10517  1re  10630  lelttr  10720  ltletr  10721  letr  10723  mul0or  11269  prodgt0  11476  mulge0b  11499  squeeze0  11532  sup2  11584  nnne0  11659  un0addcl  11918  un0mulcl  11919  nn0sub  11935  elnnz  11979  zindd  12071  rpneg  12409  xrlttri  12520  xrlelttr  12537  xrltletr  12538  xrletr  12539  qextlt  12584  qextle  12585  xmullem2  12646  xlemul1a  12669  xrsupexmnf  12686  xrinfmexpnf  12687  supxrun  12697  prunioo  12859  difreicc  12862  iccsplit  12863  uzsplit  12974  fzm1  12982  expcl2lem  13437  expeq0  13455  expnegz  13459  expaddz  13469  expmulz  13471  sqlecan  13567  facdiv  13643  facwordi  13645  bcpasc  13677  resqrex  14602  absexpz  14657  caubnd  14710  summo  15066  zsum  15067  zprod  15283  rpnnen2lem12  15570  ordvdsmul  15642  dvdsprime  16021  2mulprm  16027  ge2nprmge4  16035  prmdvdsexpr  16051  prmfac1  16053  pythagtriplem2  16144  4sqlem11  16281  vdwlem6  16312  vdwlem9  16315  vdwlem13  16319  cshwshashlem3  16423  prmlem0  16431  pleval2  17567  pltletr  17573  plelttr  17574  tsrlemax  17822  smndex1mgm  18064  f1omvdco2  18568  psgnunilem2  18615  efgredlemc  18863  frgpuptinv  18889  lt6abl  19008  dmdprdsplit2lem  19160  drngmul0or  19516  lvecvs0or  19873  domneq0  20063  baspartn  21559  0top  21588  indistopon  21606  restntr  21787  cnindis  21897  cmpfi  22013  filconn  22488  ufprim  22514  ufildr  22536  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  ovolicc2lem3  24123  rolle  24593  dvivthlem1  24611  coeaddlem  24846  dgrco  24872  plymul0or  24877  aalioulem3  24930  cxpge0  25274  cxpmul2z  25282  cxpcn3lem  25336  scvxcvx  25571  sqf11  25724  ppiublem1  25786  lgsdir2lem2  25910  lgsqrlem2  25931  2sqnn0  26022  2sqnn  26023  lmieu  26578  upgrpredgv  26932  edglnl  26936  eucrct2eupth  28030  frgrogt3nreg  28182  nvmul0or  28433  hvmul0or  28808  snsssng  30284  disjxpin  30351  subfacp1lem4  32543  satfvsucsuc  32725  satfrnmapom  32730  sat1el2xp  32739  gonarlem  32754  gonar  32755  goalrlem  32756  goalr  32757  fmlasucdisj  32759  satffunlem1lem1  32762  satffunlem2lem1  32764  untsucf  33049  sotr3  33115  dfon2lem6  33146  dftrpred3g  33185  frrlem12  33247  frrlem13  33248  nosepon  33285  nolesgn2ores  33292  nosepne  33298  nolt02o  33312  nosupbnd1lem5  33325  broutsideof2  33696  btwnoutside  33699  broutsideof3  33700  outsideoftr  33703  lineunray  33721  lineelsb2  33722  finminlem  33779  nn0prpw  33784  refssfne  33819  meran1  33872  ontgval  33892  ordcmp  33908  bj-sngltag  34419  bj-prmoore  34530  topdifinfindis  34763  icoreclin  34774  rdgssun  34795  finxpsuclem  34814  poimirlem24  35081  poimirlem25  35082  poimirlem29  35086  poimirlem31  35088  mblfinlem2  35095  ovoliunnfl  35099  itg2addnclem  35108  sdclem2  35180  fdc  35183  divrngidl  35466  lkreqN  36466  cvrnbtwn4  36575  4atlem12  36908  elpaddn0  37096  paddasslem17  37132  paddidm  37137  pmapjoin  37148  llnexchb2  37165  dalawlem13  37179  dalawlem14  37180  dochkrshp4  38685  lcfl6  38796  lcmineqlem  39340  oexpreposd  39487  nn0rppwr  39490  nn0expgcd  39492  sn-sup2  39594  fphpdo  39758  pellfundex  39827  jm2.19lem4  39933  jm2.26a  39941  relexpmulg  40411  relexp01min  40414  relexpxpmin  40418  relexpaddss  40419  clsk1indlem3  40746  or2expropbi  43626  ich2exprop  43988  poprelb  44041  reuopreuprim  44043  goldbachthlem2  44063  requad01  44139  evenltle  44235  gbowge7  44281  bgoldbtbndlem3  44325  lidldomn1  44545  uzlidlring  44553  prelrrx2b  45128  line2y  45169  itschlc0xyqsol1  45180  itsclc0xyqsolr  45183  inlinecirc02plem  45200