Theorem 3adantl3 1168

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 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  dif1ennnALT  9276  infpssrlem4  10300  fin23lem11  10311  tskwun  10778  gruf  10805  lediv2a  12107  prunioo  13457  nn0p1elfzo  13674  hashunsnggt  14353  rpnnen2lem7  16162  muldvds1  16223  muldvds2  16224  dvdscmul  16225  dvdsmulc  16226  rpexp  16658  pospropd  18279  mdetmul  22124  elcls  22576  iscnp4  22766  cnpnei  22767  cnpflf2  23503  cnpflf  23504  cnpfcf  23544  xbln0  23919  blcls  24014  iimulcl  24452  icccvx  24465  iscau2  24793  rrxcph  24908  cncombf  25174  mumul  26682  noetalem1  27241  ax5seglem1  28183  ax5seglem2  28184  wwlksnext  29144  clwwlkinwwlk  29290  nvmul0or  29898  fh1  30866  fh2  30867  cm2j  30868  pjoi0  30965  hoadddi  31051  hmopco  31271  padct  31939  iocinif  31987  volfiniune  33223  eulerpartlemb  33362  ivthALT  35215  lindsadd  36476  cnambfre  36531  rngohomco  36837  rngoisoco  36845  pexmidlem3N  38838  hdmapglem7  40795  sticksstones12a  40968  factwoffsmonot  41018  relexpmulg  42451  supxrgere  44033  supxrgelem  44037  supxrge  44038  infxr  44067  infleinflem2  44071  rexabslelem  44118  pimxrneun  44189  lptre2pt  44346  fnlimfvre  44380  limsupmnfuzlem  44432  climisp  44452  limsupgtlem  44483  dvnprodlem1  44652  ibliccsinexp  44657  iblioosinexp  44659  fourierdlem12  44825  fourierdlem41  44854  fourierdlem42  44855  fourierdlem48  44860  fourierdlem49  44861  fourierdlem51  44863  fourierdlem73  44885  fourierdlem74  44886  fourierdlem75  44887  fourierdlem97  44909  etransclem24  44964  ioorrnopnlem  45010  issalnnd  45051  sge0rpcpnf  45127  sge0seq  45152  meaiuninc3v  45190  smfmullem4  45500  smflimsupmpt  45535  smfliminfmpt  45538  lincdifsn  47095