Theorem 3adantl3 1169

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 1148	. 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  9229  infpssrlem4  10266  fin23lem11  10277  tskwun  10744  gruf  10771  lediv2a  12084  prunioo  13449  nn0p1elfzo  13670  hashunsnggt  14366  rpnnen2lem7  16195  muldvds1  16257  muldvds2  16258  dvdscmul  16259  dvdsmulc  16260  rpexp  16699  pospropd  18293  mdetmul  22517  elcls  22967  iscnp4  23157  cnpnei  23158  cnpflf2  23894  cnpflf  23895  cnpfcf  23935  xbln0  24309  blcls  24401  iimulcl  24840  icccvx  24855  iscau2  25184  rrxcph  25299  cncombf  25566  mumul  27098  noetalem1  27660  ax5seglem1  28862  ax5seglem2  28863  wwlksnext  29830  clwwlkinwwlk  29976  nvmul0or  30586  fh1  31554  fh2  31555  cm2j  31556  pjoi0  31653  hoadddi  31739  hmopco  31959  padct  32650  iocinif  32711  volfiniune  34227  eulerpartlemb  34366  ivthALT  36330  lindsadd  37614  cnambfre  37669  rngohomco  37975  rngoisoco  37983  pexmidlem3N  39973  hdmapglem7  41930  sticksstones12a  42152  relexpmulg  43706  supxrgere  45336  supxrgelem  45340  supxrge  45341  infxr  45370  infleinflem2  45374  rexabslelem  45421  pimxrneun  45491  lptre2pt  45645  fnlimfvre  45679  limsupmnfuzlem  45731  climisp  45751  limsupgtlem  45782  dvnprodlem1  45951  ibliccsinexp  45956  iblioosinexp  45958  fourierdlem12  46124  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem97  46208  etransclem24  46263  ioorrnopnlem  46309  issalnnd  46350  sge0rpcpnf  46426  sge0seq  46451  meaiuninc3v  46489  smfmullem4  46799  smflimsupmpt  46834  smfliminfmpt  46837  lincdifsn  48417  uptrlem1  49203