Theorem 3adantl3 1182

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  dif1ennnALT  9221  infpssrlem4  10263  fin23lem11  10274  tskwun  10742  gruf  10769  lediv2a  12086  prunioo  13485  nn0p1elfzo  13708  hashunsnggt  14407  rpnnen2lem7  16252  muldvds1  16314  muldvds2  16315  dvdscmul  16316  dvdsmulc  16317  rpexp  16757  pospropd  18357  mdetmul  22680  elcls  23130  iscnp4  23320  cnpnei  23321  cnpflf2  24057  cnpflf  24058  cnpfcf  24098  xbln0  24471  blcls  24563  iimulcl  24996  icccvx  25009  iscau2  25336  rrxcph  25451  cncombf  25717  mumul  27242  noetalem1  27802  ax5seglem1  29126  ax5seglem2  29127  wwlksnext  30090  clwwlkinwwlk  30239  nvmul0or  30850  fh1  31818  fh2  31819  cm2j  31820  pjoi0  31917  hoadddi  32003  hmopco  32223  padct  32917  iocinif  32980  volfiniune  34524  eulerpartlemb  34662  ivthALT  36692  axtcond  36835  lindsadd  38109  cnambfre  38164  rngohomco  38470  rngoisoco  38478  pexmidlem3N  40593  hdmapglem7  42550  sticksstones12a  42771  relexpmulg  44283  supxrgere  45906  supxrgelem  45910  supxrge  45911  infxr  45939  infleinflem2  45943  rexabslelem  45989  pimxrneun  46059  lptre2pt  46211  fnlimfvre  46245  limsupmnfuzlem  46297  climisp  46317  limsupgtlem  46348  dvnprodlem1  46517  ibliccsinexp  46522  iblioosinexp  46524  fourierdlem12  46690  fourierdlem41  46719  fourierdlem42  46720  fourierdlem48  46725  fourierdlem49  46726  fourierdlem51  46728  fourierdlem73  46750  fourierdlem74  46751  fourierdlem75  46752  fourierdlem97  46774  etransclem24  46829  ioorrnopnlem  46875  issalnnd  46916  sge0rpcpnf  46992  sge0seq  47017  meaiuninc3v  47055  smfmullem4  47365  smflimsupmpt  47400  smfliminfmpt  47403  lincdifsn  49043  uptrlem1  49828