Theorem 3ad2ant1 799

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
3ad2ant.1	|- (ph -> ch)

Assertion

Ref	Expression
3ad2ant1	|- ((ph /\ ps /\ th) -> ch)

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantr 389	. 2 |- ((ph /\ th) -> ch)
3	2	3adant2 797	1 |- ((ph /\ ps /\ th) -> ch)

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  sbciegft 1955  itlso 2858  reuuniss 2884  oneo 4202  fodomr 4469  alephval3 4883  ltasr 5189  cnegextlem1 5325  divdivmult 5759  ltmulgt11t 5810  lt2mul2divt 5830  lediv2t 5847  ledivp1 5862  ltdivp1 5863  suprleub 6014  supxrun 6040  gtndivt 6148  lbicc2t 6345  icoshftf1olem 6351  eluzp1p1t 6375  infmssuzle 6405  eluzfz1t 6427  seqzvalt 6480  seqzval2t 6493  seqzcl 6498  expwordit 6542  expword2it 6544  expubndt 6547  sqlecant 6580  bernneq2 6592  fsum1p 6965  fsumshft 6977  serz1p 6998  serzmulc1 7003  iserzgt0 7154  isummulc1 7155  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  sin02gt0 7428  tgtop11t 7584  tgsst 7586  elcls3 7661  neiint 7669  neips 7677  opnneissb 7678  opnssneib 7679  islp2 7697  iscnp2 7711  cnpco 7719  cnconst 7730  bl2in 7795  metcnpf 7835  metcnp 7839  metidcn 7852  metdnsconst 7853  cncfmet 7857  tgioolem 7866  caussi 7905  iscms2lem4 7942  grpdivval 8032  imsdval 8268  nvelbl 8276  nvcni 8279  nvlmle 8281  ipval 8300  lno0 8364  nvcnpi4 8368  nmoubi 8380  nmobndi 8383  isblo3i 8405  phpar2 8426  phpar 8427  spwval2 8595  pilem1 8609  sinq12gt0t 8644  sincosq1eq 8645  efif1lem1 8664  efif1lem2 8665  his52t 8893  bcs2t 8988  spansncol 9430  pjspansnt 9440  nmoplbt 9771  nmopubt 9772  unopt 9778  hmopt 9785  nmfnlbt 9787  nmfnleubt 9788  lnopmult 9830  nmcopexlem5 9893  nmcfnexlem5 9922  leopmult 10005  hstelt 10080  ghomid 10328  ghomf1olem 10330  truni1 10422  homeofval 10439  hmphsyma 10451  homcard 10462  fipfil2 10475  neifil 10478  filintf 10479  fgsb 10480  cnfilca 10487  mslb1 10509  2wsms 10510  1cat 10572  cmpmorp 10592  icmpmon 10623

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 776

Copyright terms: Public domain