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  9222  infpssrlem4  10259  fin23lem11  10270  tskwun  10737  gruf  10764  lediv2a  12077  prunioo  13442  nn0p1elfzo  13663  hashunsnggt  14359  rpnnen2lem7  16188  muldvds1  16250  muldvds2  16251  dvdscmul  16252  dvdsmulc  16253  rpexp  16692  pospropd  18286  mdetmul  22510  elcls  22960  iscnp4  23150  cnpnei  23151  cnpflf2  23887  cnpflf  23888  cnpfcf  23928  xbln0  24302  blcls  24394  iimulcl  24833  icccvx  24848  iscau2  25177  rrxcph  25292  cncombf  25559  mumul  27091  noetalem1  27653  ax5seglem1  28855  ax5seglem2  28856  wwlksnext  29823  clwwlkinwwlk  29969  nvmul0or  30579  fh1  31547  fh2  31548  cm2j  31549  pjoi0  31646  hoadddi  31732  hmopco  31952  padct  32643  iocinif  32704  volfiniune  34220  eulerpartlemb  34359  ivthALT  36323  lindsadd  37607  cnambfre  37662  rngohomco  37968  rngoisoco  37976  pexmidlem3N  39966  hdmapglem7  41923  sticksstones12a  42145  relexpmulg  43699  supxrgere  45329  supxrgelem  45333  supxrge  45334  infxr  45363  infleinflem2  45367  rexabslelem  45414  pimxrneun  45484  lptre2pt  45638  fnlimfvre  45672  limsupmnfuzlem  45724  climisp  45744  limsupgtlem  45775  dvnprodlem1  45944  ibliccsinexp  45949  iblioosinexp  45951  fourierdlem12  46117  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem97  46201  etransclem24  46256  ioorrnopnlem  46302  issalnnd  46343  sge0rpcpnf  46419  sge0seq  46444  meaiuninc3v  46482  smfmullem4  46792  smflimsupmpt  46827  smfliminfmpt  46830  lincdifsn  48413  uptrlem1  49199