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 579	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  9339  infpssrlem4  10375  fin23lem11  10386  tskwun  10853  gruf  10880  lediv2a  12189  prunioo  13541  nn0p1elfzo  13759  hashunsnggt  14443  rpnnen2lem7  16268  muldvds1  16329  muldvds2  16330  dvdscmul  16331  dvdsmulc  16332  rpexp  16769  pospropd  18397  mdetmul  22650  elcls  23102  iscnp4  23292  cnpnei  23293  cnpflf2  24029  cnpflf  24030  cnpfcf  24070  xbln0  24445  blcls  24540  iimulcl  24985  icccvx  25000  iscau2  25330  rrxcph  25445  cncombf  25712  mumul  27242  noetalem1  27804  ax5seglem1  28961  ax5seglem2  28962  wwlksnext  29926  clwwlkinwwlk  30072  nvmul0or  30682  fh1  31650  fh2  31651  cm2j  31652  pjoi0  31749  hoadddi  31835  hmopco  32055  padct  32733  iocinif  32786  volfiniune  34194  eulerpartlemb  34333  ivthALT  36301  lindsadd  37573  cnambfre  37628  rngohomco  37934  rngoisoco  37942  pexmidlem3N  39929  hdmapglem7  41886  sticksstones12a  42114  factwoffsmonot  42199  relexpmulg  43672  supxrgere  45248  supxrgelem  45252  supxrge  45253  infxr  45282  infleinflem2  45286  rexabslelem  45333  pimxrneun  45404  lptre2pt  45561  fnlimfvre  45595  limsupmnfuzlem  45647  climisp  45667  limsupgtlem  45698  dvnprodlem1  45867  ibliccsinexp  45872  iblioosinexp  45874  fourierdlem12  46040  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem97  46124  etransclem24  46179  ioorrnopnlem  46225  issalnnd  46266  sge0rpcpnf  46342  sge0seq  46367  meaiuninc3v  46405  smfmullem4  46715  smflimsupmpt  46750  smfliminfmpt  46753  lincdifsn  48153