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  9306  infpssrlem4  10423  fin23lem11  10434  tskwun  10908  gruf  10935  lediv2a  12251  prunioo  13652  nn0p1elfzo  13877  hashunsnggt  14579  rpnnen2lem7  16432  muldvds1  16494  muldvds2  16495  dvdscmul  16496  dvdsmulc  16497  rpexp  16942  pospropd  18549  mdetmul  22993  elcls  23446  iscnp4  23636  cnpnei  23637  cnpflf2  24374  cnpflf  24375  cnpfcf  24415  xbln0  24788  blcls  24880  iimulcl  25313  icccvx  25326  iscau2  25653  rrxcph  25768  cncombf  26034  mumul  27565  noetalem1  28155  ax5seglem1  29563  ax5seglem2  29564  wwlksnext  30539  clwwlkinwwlk  30688  nvmul0or  31309  fh1  32277  fh2  32278  cm2j  32279  pjoi0  32376  hoadddi  32462  hmopco  32682  padct  33407  iocinif  33469  volfiniune  34974  eulerpartlemb  35111  ivthALT  37338  axtcond  37481  lindsadd  38804  cnambfre  38854  rngohomco  39174  rngoisoco  39182  pexmidlem3N  41295  hdmapglem7  43252  sticksstones12a  43473  relexpmulg  44971  supxrgere  46618  supxrgelem  46622  supxrge  46623  infxr  46651  infleinflem2  46655  rexabslelem  46701  pimxrneun  46771  lptre2pt  46923  fnlimfvre  46957  limsupmnfuzlem  47009  climisp  47029  limsupgtlem  47060  dvnprodlem1  47229  ibliccsinexp  47234  iblioosinexp  47236  fourierdlem12  47402  fourierdlem41  47431  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem51  47440  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem97  47486  etransclem24  47541  ioorrnopnlem  47587  issalnnd  47628  sge0rpcpnf  47704  sge0seq  47729  meaiuninc3v  47767  smfmullem4  48077  smflimsupmpt  48112  smfliminfmpt  48115  lincdifsn  49867  uptrlem1  50657