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

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

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 1088

This theorem is referenced by:  dif1ennnALT  9177  infpssrlem4  10216  fin23lem11  10227  tskwun  10695  gruf  10722  lediv2a  12036  prunioo  13397  nn0p1elfzo  13618  hashunsnggt  14317  rpnnen2lem7  16145  muldvds1  16207  muldvds2  16208  dvdscmul  16209  dvdsmulc  16210  rpexp  16649  pospropd  18248  mdetmul  22567  elcls  23017  iscnp4  23207  cnpnei  23208  cnpflf2  23944  cnpflf  23945  cnpfcf  23985  xbln0  24358  blcls  24450  iimulcl  24889  icccvx  24904  iscau2  25233  rrxcph  25348  cncombf  25615  mumul  27147  noetalem1  27709  ax5seglem1  29001  ax5seglem2  29002  wwlksnext  29966  clwwlkinwwlk  30115  nvmul0or  30725  fh1  31693  fh2  31694  cm2j  31695  pjoi0  31792  hoadddi  31878  hmopco  32098  padct  32797  iocinif  32861  volfiniune  34387  eulerpartlemb  34525  ivthALT  36529  lindsadd  37810  cnambfre  37865  rngohomco  38171  rngoisoco  38179  pexmidlem3N  40228  hdmapglem7  42185  sticksstones12a  42407  relexpmulg  43947  supxrgere  45574  supxrgelem  45578  supxrge  45579  infxr  45607  infleinflem2  45611  rexabslelem  45658  pimxrneun  45728  lptre2pt  45880  fnlimfvre  45914  limsupmnfuzlem  45966  climisp  45986  limsupgtlem  46017  dvnprodlem1  46186  ibliccsinexp  46191  iblioosinexp  46193  fourierdlem12  46359  fourierdlem41  46388  fourierdlem42  46389  fourierdlem48  46394  fourierdlem49  46395  fourierdlem51  46397  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem97  46443  etransclem24  46498  ioorrnopnlem  46544  issalnnd  46585  sge0rpcpnf  46661  sge0seq  46686  meaiuninc3v  46724  smfmullem4  47034  smflimsupmpt  47069  smfliminfmpt  47072  lincdifsn  48666  uptrlem1  49451