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  18262  mdetmul  22486  elcls  22936  iscnp4  23126  cnpnei  23127  cnpflf2  23863  cnpflf  23864  cnpfcf  23904  xbln0  24278  blcls  24370  iimulcl  24809  icccvx  24824  iscau2  25153  rrxcph  25268  cncombf  25535  mumul  27067  noetalem1  27629  ax5seglem1  28831  ax5seglem2  28832  wwlksnext  29796  clwwlkinwwlk  29942  nvmul0or  30552  fh1  31520  fh2  31521  cm2j  31522  pjoi0  31619  hoadddi  31705  hmopco  31925  padct  32616  iocinif  32677  volfiniune  34193  eulerpartlemb  34332  ivthALT  36296  lindsadd  37580  cnambfre  37635  rngohomco  37941  rngoisoco  37949  pexmidlem3N  39939  hdmapglem7  41896  sticksstones12a  42118  relexpmulg  43672  supxrgere  45302  supxrgelem  45306  supxrge  45307  infxr  45336  infleinflem2  45340  rexabslelem  45387  pimxrneun  45457  lptre2pt  45611  fnlimfvre  45645  limsupmnfuzlem  45697  climisp  45717  limsupgtlem  45748  dvnprodlem1  45917  ibliccsinexp  45922  iblioosinexp  45924  fourierdlem12  46090  fourierdlem41  46119  fourierdlem42  46120  fourierdlem48  46125  fourierdlem49  46126  fourierdlem51  46128  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem97  46174  etransclem24  46229  ioorrnopnlem  46275  issalnnd  46316  sge0rpcpnf  46392  sge0seq  46417  meaiuninc3v  46455  smfmullem4  46765  smflimsupmpt  46800  smfliminfmpt  46803  lincdifsn  48386  uptrlem1  49172