Theorem 3adantl3 1167

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 1147	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 580	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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-an 396  df-3an 1088

This theorem is referenced by:  dif1ennnALT  9308  infpssrlem4  10343  fin23lem11  10354  tskwun  10821  gruf  10848  lediv2a  12159  prunioo  13517  nn0p1elfzo  13738  hashunsnggt  14429  rpnnen2lem7  16252  muldvds1  16314  muldvds2  16315  dvdscmul  16316  dvdsmulc  16317  rpexp  16755  pospropd  18384  mdetmul  22644  elcls  23096  iscnp4  23286  cnpnei  23287  cnpflf2  24023  cnpflf  24024  cnpfcf  24064  xbln0  24439  blcls  24534  iimulcl  24979  icccvx  24994  iscau2  25324  rrxcph  25439  cncombf  25706  mumul  27238  noetalem1  27800  ax5seglem1  28957  ax5seglem2  28958  wwlksnext  29922  clwwlkinwwlk  30068  nvmul0or  30678  fh1  31646  fh2  31647  cm2j  31648  pjoi0  31745  hoadddi  31831  hmopco  32051  padct  32736  iocinif  32789  volfiniune  34210  eulerpartlemb  34349  ivthALT  36317  lindsadd  37599  cnambfre  37654  rngohomco  37960  rngoisoco  37968  pexmidlem3N  39954  hdmapglem7  41911  sticksstones12a  42138  factwoffsmonot  42223  relexpmulg  43699  supxrgere  45282  supxrgelem  45286  supxrge  45287  infxr  45316  infleinflem2  45320  rexabslelem  45367  pimxrneun  45438  lptre2pt  45595  fnlimfvre  45629  limsupmnfuzlem  45681  climisp  45701  limsupgtlem  45732  dvnprodlem1  45901  ibliccsinexp  45906  iblioosinexp  45908  fourierdlem12  46074  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem97  46158  etransclem24  46213  ioorrnopnlem  46259  issalnnd  46300  sge0rpcpnf  46376  sge0seq  46401  meaiuninc3v  46439  smfmullem4  46749  smflimsupmpt  46784  smfliminfmpt  46787  lincdifsn  48269