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  9189  infpssrlem4  10228  fin23lem11  10239  tskwun  10707  gruf  10734  lediv2a  12048  prunioo  13409  nn0p1elfzo  13630  hashunsnggt  14329  rpnnen2lem7  16157  muldvds1  16219  muldvds2  16220  dvdscmul  16221  dvdsmulc  16222  rpexp  16661  pospropd  18260  mdetmul  22579  elcls  23029  iscnp4  23219  cnpnei  23220  cnpflf2  23956  cnpflf  23957  cnpfcf  23997  xbln0  24370  blcls  24462  iimulcl  24901  icccvx  24916  iscau2  25245  rrxcph  25360  cncombf  25627  mumul  27159  noetalem1  27721  ax5seglem1  29013  ax5seglem2  29014  wwlksnext  29978  clwwlkinwwlk  30127  nvmul0or  30738  fh1  31706  fh2  31707  cm2j  31708  pjoi0  31805  hoadddi  31891  hmopco  32111  padct  32808  iocinif  32872  volfiniune  34408  eulerpartlemb  34546  ivthALT  36551  lindsadd  37864  cnambfre  37919  rngohomco  38225  rngoisoco  38233  pexmidlem3N  40348  hdmapglem7  42305  sticksstones12a  42527  relexpmulg  44066  supxrgere  45692  supxrgelem  45696  supxrge  45697  infxr  45725  infleinflem2  45729  rexabslelem  45776  pimxrneun  45846  lptre2pt  45998  fnlimfvre  46032  limsupmnfuzlem  46084  climisp  46104  limsupgtlem  46135  dvnprodlem1  46304  ibliccsinexp  46309  iblioosinexp  46311  fourierdlem12  46477  fourierdlem41  46506  fourierdlem42  46507  fourierdlem48  46512  fourierdlem49  46513  fourierdlem51  46515  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem97  46561  etransclem24  46616  ioorrnopnlem  46662  issalnnd  46703  sge0rpcpnf  46779  sge0seq  46804  meaiuninc3v  46842  smfmullem4  47152  smflimsupmpt  47187  smfliminfmpt  47190  lincdifsn  48784  uptrlem1  49569