Theorem 3adantl3 1170

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  dif1ennnALT  9181  infpssrlem4  10222  fin23lem11  10233  tskwun  10701  gruf  10728  lediv2a  12044  prunioo  13428  nn0p1elfzo  13651  hashunsnggt  14350  rpnnen2lem7  16181  muldvds1  16243  muldvds2  16244  dvdscmul  16245  dvdsmulc  16246  rpexp  16686  pospropd  18285  mdetmul  22601  elcls  23051  iscnp4  23241  cnpnei  23242  cnpflf2  23978  cnpflf  23979  cnpfcf  24019  xbln0  24392  blcls  24484  iimulcl  24917  icccvx  24930  iscau2  25257  rrxcph  25372  cncombf  25638  mumul  27161  noetalem1  27722  ax5seglem1  29014  ax5seglem2  29015  wwlksnext  29979  clwwlkinwwlk  30128  nvmul0or  30739  fh1  31707  fh2  31708  cm2j  31709  pjoi0  31806  hoadddi  31892  hmopco  32112  padct  32809  iocinif  32872  volfiniune  34393  eulerpartlemb  34531  ivthALT  36536  axtcond  36679  lindsadd  37951  cnambfre  38006  rngohomco  38312  rngoisoco  38320  pexmidlem3N  40435  hdmapglem7  42392  sticksstones12a  42613  relexpmulg  44158  supxrgere  45784  supxrgelem  45788  supxrge  45789  infxr  45817  infleinflem2  45821  rexabslelem  45867  pimxrneun  45937  lptre2pt  46089  fnlimfvre  46123  limsupmnfuzlem  46175  climisp  46195  limsupgtlem  46226  dvnprodlem1  46395  ibliccsinexp  46400  iblioosinexp  46402  fourierdlem12  46568  fourierdlem41  46597  fourierdlem42  46598  fourierdlem48  46603  fourierdlem49  46604  fourierdlem51  46606  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem97  46652  etransclem24  46707  ioorrnopnlem  46753  issalnnd  46794  sge0rpcpnf  46870  sge0seq  46895  meaiuninc3v  46933  smfmullem4  47243  smflimsupmpt  47278  smfliminfmpt  47281  lincdifsn  48915  uptrlem1  49700