Theorem 3ad2ant3 961

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 271	. 2 |- ( ( th /\ ph ) -> ch )
3	2	3adant1 956	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simp3l  966  simp3r  967  simp31  974  simp32  975  simp33  976  simp3ll  1009  simp3lr  1010  simp3rl  1011  simp3rr  1012  simp3l1  1043  simp3l2  1044  simp3l3  1045  simp3r1  1046  simp3r2  1047  simp3r3  1048  simp31l  1061  simp31r  1062  simp32l  1063  simp32r  1064  simp33l  1065  simp33r  1066  simp311  1085  simp312  1086  simp313  1087  simp321  1088  simp322  1089  simp323  1090  simp331  1091  simp332  1092  simp333  1093  3anim123i  1123  3jaao  1239  ceqsalt  2625  ceqsralt  2626  vtoclgft  2649  ifbothdc  3380  tpssi  3551  sotricim  4078  elirr  4284  en2lp  4297  reg3exmidlemwe  4321  sotri2  4742  poltletr  4745  funprg  4969  funtpg  4970  fntpg  4975  funimaexglem  5002  fvun1  5260  ftpg  5368  fsnunf  5383  fsnunfv  5384  caovimo  5714  brtposg  5892  smoel  5938  rdgivallem  5991  frecsuclem1  6010  frecsuclemdm  6011  frecsuclem2  6012  frecsuclem3  6013  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  ltsopi  6510  distrnqg  6577  ltmnqg  6591  mulcanenq0ec  6635  distrnq0  6649  prarloclem5  6690  1idprl  6780  1idpru  6781  ltaprg  6809  recexprlemopl  6815  recexprlemopu  6817  recexprlem1ssl  6823  aptipr  6831  ltmprr  6832  cauappcvgprlemlol  6837  cauappcvgprlemupu  6839  caucvgprlemlol  6860  caucvgprlemupu  6862  caucvgprprlemlol  6888  caucvgprprlemupu  6890  readdcan  7248  cnegexlem2  7284  addcan2  7289  ltadd2  7523  apreap  7687  ltmul1  7692  apcotr  7707  apadd1  7708  mulext1  7712  divdirap  7785  divcanap5  7802  ltdiv1  7946  lt2halves  8266  zdivmul  8437  eluzsub  8648  ledivge1le  8803  addlelt  8839  elioo5  8956  iccsupr  8989  iccneg  9011  icoshft  9012  icoshftf1o  9013  zltaddlt1le  9028  fzen  9062  elfz1b  9107  fzrevral  9122  fzshftral  9125  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  fz0fzdiffz0  9141  elfzo  9159  elfzonlteqm1  9219  modqaddmulmod  9393  expdivap  9527  leexp2a  9529  bcval3  9678  shftfibg  9708  elicc4abs  9980  mulcn2  10151  dvdsval2  10198  dvdsmulcr  10225  modmulconst  10227  dvdsexp  10261  oddge22np1  10281  modremain  10329  mulgcd  10405  mulgcdr  10407  gcddiv  10408  rpmulgcd  10415  rplpwr  10416  coprmdvds  10474  cncongr1  10485  dvdsnprmd  10507  prmexpb  10530  rpexp  10532  cncongrprm  10536  findset  10740