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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  dif1ennnALT  9275  infpssrlem4  10391  fin23lem11  10402  tskwun  10876  gruf  10903  lediv2a  12218  prunioo  13619  nn0p1elfzo  13844  hashunsnggt  14545  rpnnen2lem7  16397  muldvds1  16459  muldvds2  16460  dvdscmul  16461  dvdsmulc  16462  rpexp  16907  pospropd  18508  mdetmul  22947  elcls  23400  iscnp4  23590  cnpnei  23591  cnpflf2  24328  cnpflf  24329  cnpfcf  24369  xbln0  24742  blcls  24834  iimulcl  25267  icccvx  25280  iscau2  25607  rrxcph  25722  cncombf  25988  mumul  27517  noetalem1  28107  ax5seglem1  29515  ax5seglem2  29516  wwlksnext  30491  clwwlkinwwlk  30640  nvmul0or  31261  fh1  32229  fh2  32230  cm2j  32231  pjoi0  32328  hoadddi  32414  hmopco  32634  padct  33361  iocinif  33423  volfiniune  34913  eulerpartlemb  35050  ivthALT  37219  axtcond  37362  lindsadd  38645  cnambfre  38695  rngohomco  39017  rngoisoco  39025  pexmidlem3N  41138  hdmapglem7  43095  sticksstones12a  43316  relexpmulg  44819  supxrgere  46453  supxrgelem  46457  supxrge  46458  infxr  46486  infleinflem2  46490  rexabslelem  46536  pimxrneun  46606  lptre2pt  46758  fnlimfvre  46792  limsupmnfuzlem  46844  climisp  46864  limsupgtlem  46895  dvnprodlem1  47064  ibliccsinexp  47069  iblioosinexp  47071  fourierdlem12  47237  fourierdlem41  47266  fourierdlem42  47267  fourierdlem48  47272  fourierdlem49  47273  fourierdlem51  47275  fourierdlem73  47297  fourierdlem74  47298  fourierdlem75  47299  fourierdlem97  47321  etransclem24  47376  ioorrnopnlem  47422  issalnnd  47463  sge0rpcpnf  47539  sge0seq  47564  meaiuninc3v  47602  smfmullem4  47912  smflimsupmpt  47947  smfliminfmpt  47950  lincdifsn  49644  uptrlem1  50434