Theorem 3adantl3 1187

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  dif1ennnALT  9244  infpssrlem4  10305  fin23lem11  10316  tskwun  10784  gruf  10811  lediv2a  12124  prunioo  13524  nn0p1elfzo  13748  hashunsnggt  14448  rpnnen2lem7  16298  muldvds1  16360  muldvds2  16361  dvdscmul  16362  dvdsmulc  16363  rpexp  16803  pospropd  18403  mdetmul  22830  elcls  23280  iscnp4  23470  cnpnei  23471  cnpflf2  24208  cnpflf  24209  cnpfcf  24249  xbln0  24622  blcls  24714  iimulcl  25147  icccvx  25160  iscau2  25487  rrxcph  25602  cncombf  25868  mumul  27396  noetalem1  27956  ax5seglem1  29333  ax5seglem2  29334  wwlksnext  30309  clwwlkinwwlk  30458  nvmul0or  31073  fh1  32041  fh2  32042  cm2j  32043  pjoi0  32140  hoadddi  32226  hmopco  32446  padct  33133  iocinif  33196  volfiniune  34685  eulerpartlemb  34823  ivthALT  36903  axtcond  37046  lindsadd  38321  cnambfre  38376  rngohomco  38683  rngoisoco  38691  pexmidlem3N  40804  hdmapglem7  42761  sticksstones12a  42982  relexpmulg  44494  supxrgere  46107  supxrgelem  46111  supxrge  46112  infxr  46140  infleinflem2  46144  rexabslelem  46190  pimxrneun  46260  lptre2pt  46412  fnlimfvre  46446  limsupmnfuzlem  46498  climisp  46518  limsupgtlem  46549  dvnprodlem1  46718  ibliccsinexp  46723  iblioosinexp  46725  fourierdlem12  46891  fourierdlem41  46920  fourierdlem42  46921  fourierdlem48  46926  fourierdlem49  46927  fourierdlem51  46929  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem97  46975  etransclem24  47030  ioorrnopnlem  47076  issalnnd  47117  sge0rpcpnf  47193  sge0seq  47218  meaiuninc3v  47256  smfmullem4  47566  smflimsupmpt  47601  smfliminfmpt  47604  lincdifsn  49261  uptrlem1  50045