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 591	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  dif1ennnALT  9233  infpssrlem4  10285  fin23lem11  10296  tskwun  10764  gruf  10791  lediv2a  12104  prunioo  13503  nn0p1elfzo  13727  hashunsnggt  14426  rpnnen2lem7  16271  muldvds1  16333  muldvds2  16334  dvdscmul  16335  dvdsmulc  16336  rpexp  16776  pospropd  18376  mdetmul  22780  elcls  23230  iscnp4  23420  cnpnei  23421  cnpflf2  24157  cnpflf  24158  cnpfcf  24198  xbln0  24571  blcls  24663  iimulcl  25096  icccvx  25109  iscau2  25436  rrxcph  25551  cncombf  25817  mumul  27345  noetalem1  27905  ax5seglem1  29278  ax5seglem2  29279  wwlksnext  30242  clwwlkinwwlk  30391  nvmul0or  31002  fh1  31970  fh2  31971  cm2j  31972  pjoi0  32069  hoadddi  32155  hmopco  32375  padct  33063  iocinif  33126  volfiniune  34620  eulerpartlemb  34758  ivthALT  36846  axtcond  36989  lindsadd  38264  cnambfre  38319  rngohomco  38625  rngoisoco  38633  pexmidlem3N  40746  hdmapglem7  42703  sticksstones12a  42924  relexpmulg  44436  supxrgere  46049  supxrgelem  46053  supxrge  46054  infxr  46082  infleinflem2  46086  rexabslelem  46132  pimxrneun  46202  lptre2pt  46354  fnlimfvre  46388  limsupmnfuzlem  46440  climisp  46460  limsupgtlem  46491  dvnprodlem1  46660  ibliccsinexp  46665  iblioosinexp  46667  fourierdlem12  46833  fourierdlem41  46862  fourierdlem42  46863  fourierdlem48  46868  fourierdlem49  46869  fourierdlem51  46871  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem97  46917  etransclem24  46972  ioorrnopnlem  47018  issalnnd  47059  sge0rpcpnf  47135  sge0seq  47160  meaiuninc3v  47198  smfmullem4  47508  smflimsupmpt  47543  smfliminfmpt  47546  lincdifsn  49204  uptrlem1  49988