Theorem 3ad2ant3 978

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantl 452	. 2 |- ((th /\ ph) -> ch)
3	2	3adant1 973	1 |- ((ps /\ th /\ ph) -> ch)

Syntax hints:   -> wi 4   /\ w3a 934

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 177  df-an 360  df-3an 936

This theorem is referenced by:  simp3l  983  simp3r  984  simp31  991  simp32  992  simp33  993  simp3ll  1026  simp3lr  1027  simp3rl  1028  simp3rr  1029  simp3l1  1060  simp3l2  1061  simp3l3  1062  simp3r1  1063  simp3r2  1064  simp3r3  1065  simp31l  1078  simp31r  1079  simp32l  1080  simp32r  1081  simp33l  1082  simp33r  1083  simp311  1102  simp312  1103  simp313  1104  simp321  1105  simp322  1106  simp323  1107  simp331  1108  simp332  1109  simp333  1110  3anim123i  1137  3jaao  1249  ceqsalt  2882  ceqsralt  2883  vtoclgft  2906  nnsucelrlem3  4427  nnsucelr  4429  ltfintri  4467  ssfin  4471  tfin11  4494  tfinltfinlem1  4501  sfintfin  4533  sfin111  4537  funprg  5150  fnprg  5154  fvun1  5380  ider  5944  ssetpov  5945  eqer  5962  elmapg  6013  elpmg  6014  ener  6040  enadj  6061  enprmaplem6  6082  nenpw1pwlem2  6086  elce  6176  addlec  6209  lenc  6224  taddc  6230