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  9281  infpssrlem4  10318  fin23lem11  10329  tskwun  10796  gruf  10823  lediv2a  12134  prunioo  13496  nn0p1elfzo  13717  hashunsnggt  14410  rpnnen2lem7  16236  muldvds1  16298  muldvds2  16299  dvdscmul  16300  dvdsmulc  16301  rpexp  16739  pospropd  18335  mdetmul  22559  elcls  23009  iscnp4  23199  cnpnei  23200  cnpflf2  23936  cnpflf  23937  cnpfcf  23977  xbln0  24351  blcls  24443  iimulcl  24882  icccvx  24897  iscau2  25227  rrxcph  25342  cncombf  25609  mumul  27141  noetalem1  27703  ax5seglem1  28853  ax5seglem2  28854  wwlksnext  29821  clwwlkinwwlk  29967  nvmul0or  30577  fh1  31545  fh2  31546  cm2j  31547  pjoi0  31644  hoadddi  31730  hmopco  31950  padct  32643  iocinif  32704  volfiniune  34207  eulerpartlemb  34346  ivthALT  36299  lindsadd  37583  cnambfre  37638  rngohomco  37944  rngoisoco  37952  pexmidlem3N  39937  hdmapglem7  41894  sticksstones12a  42116  factwoffsmonot  42201  relexpmulg  43681  supxrgere  45308  supxrgelem  45312  supxrge  45313  infxr  45342  infleinflem2  45346  rexabslelem  45393  pimxrneun  45463  lptre2pt  45617  fnlimfvre  45651  limsupmnfuzlem  45703  climisp  45723  limsupgtlem  45754  dvnprodlem1  45923  ibliccsinexp  45928  iblioosinexp  45930  fourierdlem12  46096  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem97  46180  etransclem24  46235  ioorrnopnlem  46281  issalnnd  46322  sge0rpcpnf  46398  sge0seq  46423  meaiuninc3v  46461  smfmullem4  46771  smflimsupmpt  46806  smfliminfmpt  46809  lincdifsn  48348