Theorem 3adantl3 1169

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 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  dif1ennnALT  9277  infpssrlem4  10301  fin23lem11  10312  tskwun  10779  gruf  10806  lediv2a  12108  prunioo  13458  nn0p1elfzo  13675  hashunsnggt  14354  rpnnen2lem7  16163  muldvds1  16224  muldvds2  16225  dvdscmul  16226  dvdsmulc  16227  rpexp  16659  pospropd  18280  mdetmul  22125  elcls  22577  iscnp4  22767  cnpnei  22768  cnpflf2  23504  cnpflf  23505  cnpfcf  23545  xbln0  23920  blcls  24015  iimulcl  24453  icccvx  24466  iscau2  24794  rrxcph  24909  cncombf  25175  mumul  26685  noetalem1  27244  ax5seglem1  28186  ax5seglem2  28187  wwlksnext  29147  clwwlkinwwlk  29293  nvmul0or  29903  fh1  30871  fh2  30872  cm2j  30873  pjoi0  30970  hoadddi  31056  hmopco  31276  padct  31944  iocinif  31992  volfiniune  33228  eulerpartlemb  33367  ivthALT  35220  lindsadd  36481  cnambfre  36536  rngohomco  36842  rngoisoco  36850  pexmidlem3N  38843  hdmapglem7  40800  sticksstones12a  40973  factwoffsmonot  41023  relexpmulg  42461  supxrgere  44043  supxrgelem  44047  supxrge  44048  infxr  44077  infleinflem2  44081  rexabslelem  44128  pimxrneun  44199  lptre2pt  44356  fnlimfvre  44390  limsupmnfuzlem  44442  climisp  44462  limsupgtlem  44493  dvnprodlem1  44662  ibliccsinexp  44667  iblioosinexp  44669  fourierdlem12  44835  fourierdlem41  44864  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem51  44873  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem97  44919  etransclem24  44974  ioorrnopnlem  45020  issalnnd  45061  sge0rpcpnf  45137  sge0seq  45162  meaiuninc3v  45200  smfmullem4  45510  smflimsupmpt  45545  smfliminfmpt  45548  lincdifsn  47105