Theorem 3ad2ant1 925

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

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 261	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant2 923	1 |- ( ( ph /\ ps /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simp1l  928  simp1r  929  simp11  934  simp12  935  simp13  936  simp1ll  967  simp1lr  968  simp1rl  969  simp1rr  970  simp1l1  997  simp1l2  998  simp1l3  999  simp1r1  1000  simp1r2  1001  simp1r3  1002  simp11l  1015  simp11r  1016  simp12l  1017  simp12r  1018  simp13l  1019  simp13r  1020  simp111  1033  simp112  1034  simp113  1035  simp121  1036  simp122  1037  simp123  1038  simp131  1039  simp132  1040  simp133  1041  3anim123i  1089  3jaao  1203  ceqsalt  2580  sbciegft  2793  reupick2  3223  ifbothdc  3357  frirrg  4087  breldmg  4541  fntpg  4955  funimaexglem  4982  fex2  5059  fvun1  5239  fprg  5346  fsnunfv  5363  fnfvima  5393  cocan1  5427  cocan2  5428  mpt2fvex  5829  poxp  5853  smoiso  5917  tfrlem5  5930  tfrlemibxssdm  5941  nnawordex  6101  fidceq  6330  fidifsnen  6331  dif1en  6337  ordiso2  6357  mulcanenq0ec  6543  prltlu  6585  prarloclem3step  6594  prarloclem5  6598  ltasrg  6855  cnegexlem1  7186  addcan  7191  apcotr  7598  apadd1  7599  mulext1  7603  divdivap1  7699  divdivap2  7700  div2negap  7711  divneg2ap  7712  ltmulgt11  7830  ltdiv2  7853  squeeze0  7870  nndivtr  7955  nn0n0n1ge2  8311  zdivmul  8330  gtndiv  8335  eluzuzle  8481  eluzp1p1  8498  qdivcl  8577  irrmul  8581  rpgecl  8611  lbico1  8799  lbicc2  8852  uzsubsubfz  8911  elfz1b  8952  elfz0ubfz0  8982  fz0fzelfz0  8984  difelfzle  8992  difelfznle  8993  2ffzeq  8998  fzo1fzo0n0  9039  ubmelfzo  9056  fzonn0p1p1  9069  elfzom1p1elfzo  9070  elfzonelfzo  9086  subfzo0  9097  ceiqle  9155  ceilqle  9156  modqval  9166  flqpmodeq  9169  modq0  9171  negqmod0  9173  modqge0  9174  modqlt  9175  modqdiffl  9177  modqmulnn  9184  qexpclz  9276  expgt1  9293  expp1zap  9303  expm1ap  9304  expubnd  9311  bernneq2  9370  expnlbnd  9373  shftuz  9418  mulreap  9464  redivap  9474  imdivap  9481  resqrtcl  9627  climuni  9814  addcn2  9831  mulcn2  9833  bdfind  10071