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  9175  infpssrlem4  10214  fin23lem11  10225  tskwun  10693  gruf  10720  lediv2a  12034  prunioo  13395  nn0p1elfzo  13616  hashunsnggt  14315  rpnnen2lem7  16143  muldvds1  16205  muldvds2  16206  dvdscmul  16207  dvdsmulc  16208  rpexp  16647  pospropd  18246  mdetmul  22565  elcls  23015  iscnp4  23205  cnpnei  23206  cnpflf2  23942  cnpflf  23943  cnpfcf  23983  xbln0  24356  blcls  24448  iimulcl  24887  icccvx  24902  iscau2  25231  rrxcph  25346  cncombf  25613  mumul  27145  noetalem1  27707  ax5seglem1  28950  ax5seglem2  28951  wwlksnext  29915  clwwlkinwwlk  30064  nvmul0or  30674  fh1  31642  fh2  31643  cm2j  31644  pjoi0  31741  hoadddi  31827  hmopco  32047  padct  32746  iocinif  32810  volfiniune  34336  eulerpartlemb  34474  ivthALT  36478  lindsadd  37753  cnambfre  37808  rngohomco  38114  rngoisoco  38122  pexmidlem3N  40171  hdmapglem7  42128  sticksstones12a  42350  relexpmulg  43893  supxrgere  45520  supxrgelem  45524  supxrge  45525  infxr  45553  infleinflem2  45557  rexabslelem  45604  pimxrneun  45674  lptre2pt  45826  fnlimfvre  45860  limsupmnfuzlem  45912  climisp  45932  limsupgtlem  45963  dvnprodlem1  46132  ibliccsinexp  46137  iblioosinexp  46139  fourierdlem12  46305  fourierdlem41  46334  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem97  46389  etransclem24  46444  ioorrnopnlem  46490  issalnnd  46531  sge0rpcpnf  46607  sge0seq  46632  meaiuninc3v  46670  smfmullem4  46980  smflimsupmpt  47015  smfliminfmpt  47018  lincdifsn  48612  uptrlem1  49397