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  9166  infpssrlem4  10200  fin23lem11  10211  tskwun  10678  gruf  10705  lediv2a  12019  prunioo  13384  nn0p1elfzo  13605  hashunsnggt  14301  rpnnen2lem7  16129  muldvds1  16191  muldvds2  16192  dvdscmul  16193  dvdsmulc  16194  rpexp  16633  pospropd  18231  mdetmul  22508  elcls  22958  iscnp4  23148  cnpnei  23149  cnpflf2  23885  cnpflf  23886  cnpfcf  23926  xbln0  24300  blcls  24392  iimulcl  24831  icccvx  24846  iscau2  25175  rrxcph  25290  cncombf  25557  mumul  27089  noetalem1  27651  ax5seglem1  28873  ax5seglem2  28874  wwlksnext  29838  clwwlkinwwlk  29984  nvmul0or  30594  fh1  31562  fh2  31563  cm2j  31564  pjoi0  31661  hoadddi  31747  hmopco  31967  padct  32662  iocinif  32724  volfiniune  34197  eulerpartlemb  34336  ivthALT  36309  lindsadd  37593  cnambfre  37648  rngohomco  37954  rngoisoco  37962  pexmidlem3N  39951  hdmapglem7  41908  sticksstones12a  42130  relexpmulg  43683  supxrgere  45313  supxrgelem  45317  supxrge  45318  infxr  45346  infleinflem2  45350  rexabslelem  45397  pimxrneun  45467  lptre2pt  45621  fnlimfvre  45655  limsupmnfuzlem  45707  climisp  45727  limsupgtlem  45758  dvnprodlem1  45927  ibliccsinexp  45932  iblioosinexp  45934  fourierdlem12  46100  fourierdlem41  46129  fourierdlem42  46130  fourierdlem48  46135  fourierdlem49  46136  fourierdlem51  46138  fourierdlem73  46160  fourierdlem74  46161  fourierdlem75  46162  fourierdlem97  46184  etransclem24  46239  ioorrnopnlem  46285  issalnnd  46326  sge0rpcpnf  46402  sge0seq  46427  meaiuninc3v  46465  smfmullem4  46775  smflimsupmpt  46810  smfliminfmpt  46813  lincdifsn  48409  uptrlem1  49195