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  9161  infpssrlem4  10197  fin23lem11  10208  tskwun  10675  gruf  10702  lediv2a  12016  prunioo  13381  nn0p1elfzo  13602  hashunsnggt  14301  rpnnen2lem7  16129  muldvds1  16191  muldvds2  16192  dvdscmul  16193  dvdsmulc  16194  rpexp  16633  pospropd  18231  mdetmul  22538  elcls  22988  iscnp4  23178  cnpnei  23179  cnpflf2  23915  cnpflf  23916  cnpfcf  23956  xbln0  24329  blcls  24421  iimulcl  24860  icccvx  24875  iscau2  25204  rrxcph  25319  cncombf  25586  mumul  27118  noetalem1  27680  ax5seglem1  28906  ax5seglem2  28907  wwlksnext  29871  clwwlkinwwlk  30020  nvmul0or  30630  fh1  31598  fh2  31599  cm2j  31600  pjoi0  31697  hoadddi  31783  hmopco  32003  padct  32701  iocinif  32764  volfiniune  34243  eulerpartlemb  34381  ivthALT  36377  lindsadd  37661  cnambfre  37716  rngohomco  38022  rngoisoco  38030  pexmidlem3N  40019  hdmapglem7  41976  sticksstones12a  42198  relexpmulg  43751  supxrgere  45380  supxrgelem  45384  supxrge  45385  infxr  45413  infleinflem2  45417  rexabslelem  45464  pimxrneun  45534  lptre2pt  45686  fnlimfvre  45720  limsupmnfuzlem  45772  climisp  45792  limsupgtlem  45823  dvnprodlem1  45992  ibliccsinexp  45997  iblioosinexp  45999  fourierdlem12  46165  fourierdlem41  46194  fourierdlem42  46195  fourierdlem48  46200  fourierdlem49  46201  fourierdlem51  46203  fourierdlem73  46225  fourierdlem74  46226  fourierdlem75  46227  fourierdlem97  46249  etransclem24  46304  ioorrnopnlem  46350  issalnnd  46391  sge0rpcpnf  46467  sge0seq  46492  meaiuninc3v  46530  smfmullem4  46840  smflimsupmpt  46875  smfliminfmpt  46878  lincdifsn  48464  uptrlem1  49250