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  9198  infpssrlem4  10235  fin23lem11  10246  tskwun  10713  gruf  10740  lediv2a  12053  prunioo  13418  nn0p1elfzo  13639  hashunsnggt  14335  rpnnen2lem7  16164  muldvds1  16226  muldvds2  16227  dvdscmul  16228  dvdsmulc  16229  rpexp  16668  pospropd  18266  mdetmul  22543  elcls  22993  iscnp4  23183  cnpnei  23184  cnpflf2  23920  cnpflf  23921  cnpfcf  23961  xbln0  24335  blcls  24427  iimulcl  24866  icccvx  24881  iscau2  25210  rrxcph  25325  cncombf  25592  mumul  27124  noetalem1  27686  ax5seglem1  28908  ax5seglem2  28909  wwlksnext  29873  clwwlkinwwlk  30019  nvmul0or  30629  fh1  31597  fh2  31598  cm2j  31599  pjoi0  31696  hoadddi  31782  hmopco  32002  padct  32693  iocinif  32754  volfiniune  34213  eulerpartlemb  34352  ivthALT  36316  lindsadd  37600  cnambfre  37655  rngohomco  37961  rngoisoco  37969  pexmidlem3N  39959  hdmapglem7  41916  sticksstones12a  42138  relexpmulg  43692  supxrgere  45322  supxrgelem  45326  supxrge  45327  infxr  45356  infleinflem2  45360  rexabslelem  45407  pimxrneun  45477  lptre2pt  45631  fnlimfvre  45665  limsupmnfuzlem  45717  climisp  45737  limsupgtlem  45768  dvnprodlem1  45937  ibliccsinexp  45942  iblioosinexp  45944  fourierdlem12  46110  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem97  46194  etransclem24  46249  ioorrnopnlem  46295  issalnnd  46336  sge0rpcpnf  46412  sge0seq  46437  meaiuninc3v  46475  smfmullem4  46785  smflimsupmpt  46820  smfliminfmpt  46823  lincdifsn  48406  uptrlem1  49192