Theorem 3adantl3 1175

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 1154	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 586	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  dif1ennnALT  9177  infpssrlem4  10219  fin23lem11  10230  tskwun  10698  gruf  10725  lediv2a  12041  prunioo  13425  nn0p1elfzo  13648  hashunsnggt  14347  rpnnen2lem7  16178  muldvds1  16240  muldvds2  16241  dvdscmul  16242  dvdsmulc  16243  rpexp  16683  pospropd  18282  mdetmul  22606  elcls  23056  iscnp4  23246  cnpnei  23247  cnpflf2  23983  cnpflf  23984  cnpfcf  24024  xbln0  24397  blcls  24489  iimulcl  24922  icccvx  24935  iscau2  25262  rrxcph  25377  cncombf  25643  mumul  27162  noetalem1  27723  ax5seglem1  29015  ax5seglem2  29016  wwlksnext  29979  clwwlkinwwlk  30128  nvmul0or  30739  fh1  31707  fh2  31708  cm2j  31709  pjoi0  31806  hoadddi  31892  hmopco  32112  padct  32810  iocinif  32873  volfiniune  34414  eulerpartlemb  34552  ivthALT  36563  axtcond  36706  lindsadd  37980  cnambfre  38035  rngohomco  38341  rngoisoco  38349  pexmidlem3N  40464  hdmapglem7  42421  sticksstones12a  42642  relexpmulg  44154  supxrgere  45778  supxrgelem  45782  supxrge  45783  infxr  45811  infleinflem2  45815  rexabslelem  45861  pimxrneun  45931  lptre2pt  46083  fnlimfvre  46117  limsupmnfuzlem  46169  climisp  46189  limsupgtlem  46220  dvnprodlem1  46389  ibliccsinexp  46394  iblioosinexp  46396  fourierdlem12  46562  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem97  46646  etransclem24  46701  ioorrnopnlem  46747  issalnnd  46788  sge0rpcpnf  46864  sge0seq  46889  meaiuninc3v  46927  smfmullem4  47237  smflimsupmpt  47272  smfliminfmpt  47275  lincdifsn  48915  uptrlem1  49700