Theorem jaodan 972

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Assertion

Ref	Expression
jaodan	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 418	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 418	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 873	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 412	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  mpjaodan  973  andi  1025  ccase  1053  relop  5838  poltletr  6144  ordnbtwn  6484  eqfnun  7067  oeoa  8644  oeoe  8646  ssnnfi  9223  domnsymfi  9253  unwdomg  9615  numwdom  10177  infpssrlem5  10424  fin23lem24  10439  fin23lem28  10457  fin1a2lem10  10526  zornn0g  10622  gchdomtri  10753  fpwwe2lem11  10765  fpwwe2lem12  10766  msqgt0  11876  recextlem2  11987  lemul1a  12211  nnne0  12412  nnnn0addcl  12676  un0addcl  12679  un0mulcl  12680  elz2  12751  mul2lt0bi  13268  xaddnemnf  13406  xaddnepnf  13407  rexmul  13441  xlemul1a  13458  xrsupsslem  13477  xrinfmsslem  13478  ixxun  13532  fzsplit2  13723  fzsuc2  13756  elfzp12  13777  seqf1olem2  14225  expp1  14251  expneg  14252  expcllem  14255  mulexpz  14285  expaddz  14289  expmulz  14291  zzlesq  14390  faclbnd4lem3  14480  faclbnd4lem4  14481  faclbnd4  14482  bcpasc  14506  ccatass  14775  ccatrn  14776  ccatswrd  14860  ccatpfx  14892  cats1un  14912  revccat  14957  summo  15927  sumss2  15936  fsumsplit  15951  geomulcvg  16089  fprodsplit  16177  bpoly2  16267  bpoly3  16268  ef0lem  16288  odd2np1  16555  sadcaddlem  16671  gcdcllem3  16715  dvdslcm  16817  lcmeq0  16819  lcmcl  16820  lcmneg  16822  lcmgcd  16826  rpexp1i  16943  pcid  17095  4sqlem16  17182  funcres2c  18128  lubun  18739  mulgneg  19352  mulgnn0z  19361  frgpup3lem  20042  gsumzunsnd  20221  gsumunsnfd  20222  dprddisj2  20306  dmdprdsplit2  20313  dprdsplit  20315  gsumdixp  20599  lssvs0or  21439  evlslem4  22440  refun0  23889  txhaus  24021  xkoptsub  24028  ptunhmeo  24182  xpsxmetlem  24753  xpsmet  24756  mbfss  26022  itg1addlem2  26073  iblss2  26181  itgsplit  26211  limcres  26261  ftc1lem5  26415  coe1mul3  26472  dgrlt  26640  abelthlem3  26817  atanlogaddlem  27298  atanlogsub  27301  atans2  27316  efrlim  27354  bposlem2  27669  lgsdir2lem4  27712  2sqb  27816  pntpbnd1  27970  ostthlem1  28011  nosepdm  28098  nosupbnd2lem1  28129  negsid  28484  elzn0s  28841  zsbday  28849  zcuts  28850  expsp1  28872  hlbtwn  29134  cgracol  29393  inaghl  29421  brbtwn2  29540  axcontlem2  29600  ifnebib  33243  isoun  33392  eliccelico  33465  elicoelioo  33466  fzsplit3  33481  prodpr  33513  zarclsun  34613  xrge0iifhom  34680  esumsplit  34796  esumpad2  34799  sibfinima  35082  circlemethhgt  35383  bnj1137  35736  subfacp1lem4  36156  subfacp1lem5  36157  mclsax  36542  poimirlem2  38808  poimirlem8  38814  poimirlem22  38828  poimirlem28  38834  ftc1cnnc  38878  ftc1anclem2  38880  dfprop1  38913  fdc  38945  incsequz2  38949  unichnidl  39231  lkrss2N  40492  cdlemg27b  42019  tendoex  42298  dihmeetlem2N  42622  dvh3dim3N  42772  aks6d1c2p2  43435  hashscontpow  43438  aks6d1c5  43455  sticksstones1  43462  sticksstones2  43463  unitscyglem2  43512  ofun  43556  sn-nnne0  43790  nn0addcom  43792  nn0mulcom  43796  zmulcomlem  43797  rexzrexnn0  44077  pell14qrexpcl  44140  elpell1qr2  44145  acongeq  44256  jm2.23  44269  rpnnen3  44305  mnringmulrcld  45487  mnuprdlem3  45519  radcnvrat  45559  sumpair  46326  cncfiooicclem1  47176  fourierdlem80  47469  fourierdlem93  47482  fullthinc  50916  veronesevrowd  51407