Theorem 3adantl3 1187

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3adantl.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adantl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl3

Step	Hyp	Ref	Expression
1		3simpa 1166	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 592	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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-3an 1105

This theorem is used by:  dif1ennnALT  9261  infpssrlem4  10377  fin23lem11  10388  tskwun  10862  gruf  10889  lediv2a  12204  prunioo  13605  nn0p1elfzo  13830  hashunsnggt  14531  rpnnen2lem7  16381  muldvds1  16443  muldvds2  16444  dvdscmul  16445  dvdsmulc  16446  rpexp  16891  pospropd  18492  mdetmul  22931  elcls  23384  iscnp4  23574  cnpnei  23575  cnpflf2  24312  cnpflf  24313  cnpfcf  24353  xbln0  24726  blcls  24818  iimulcl  25251  icccvx  25264  iscau2  25591  rrxcph  25706  cncombf  25972  mumul  27501  noetalem1  28091  ax5seglem1  29499  ax5seglem2  29500  wwlksnext  30475  clwwlkinwwlk  30624  nvmul0or  31245  fh1  32213  fh2  32214  cm2j  32215  pjoi0  32312  hoadddi  32398  hmopco  32618  padct  33303  iocinif  33366  volfiniune  34856  eulerpartlemb  34993  ivthALT  37103  axtcond  37246  lindsadd  38516  cnambfre  38566  rngohomco  38888  rngoisoco  38896  pexmidlem3N  41009  hdmapglem7  42966  sticksstones12a  43187  relexpmulg  44695  supxrgere  46314  supxrgelem  46318  supxrge  46319  infxr  46347  infleinflem2  46351  rexabslelem  46397  pimxrneun  46467  lptre2pt  46619  fnlimfvre  46653  limsupmnfuzlem  46705  climisp  46725  limsupgtlem  46756  dvnprodlem1  46925  ibliccsinexp  46930  iblioosinexp  46932  fourierdlem12  47098  fourierdlem41  47127  fourierdlem42  47128  fourierdlem48  47133  fourierdlem49  47134  fourierdlem51  47136  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem97  47182  etransclem24  47237  ioorrnopnlem  47283  issalnnd  47324  sge0rpcpnf  47400  sge0seq  47425  meaiuninc3v  47463  smfmullem4  47773  smflimsupmpt  47808  smfliminfmpt  47811  lincdifsn  49505  uptrlem1  50287