Theorem 3ad2ant3 985

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

Syntax hints:   -> wi 4   /\ w3a 943

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

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  simp3l  990  simp3r  991  simp31  998  simp32  999  simp33  1000  simp3ll  1033  simp3lr  1034  simp3rl  1035  simp3rr  1036  simp3l1  1067  simp3l2  1068  simp3l3  1069  simp3r1  1070  simp3r2  1071  simp3r3  1072  simp31l  1085  simp31r  1086  simp32l  1087  simp32r  1088  simp33l  1089  simp33r  1090  simp311  1109  simp312  1110  simp313  1111  simp321  1112  simp322  1113  simp323  1114  simp331  1115  simp332  1116  simp333  1117  3anim123i  1147  3jaao  1267  ceqsalt  2681  ceqsralt  2682  vtoclgft  2705  ifbothdc  3468  tpssi  3650  sotricim  4203  elirr  4414  en2lp  4427  reg3exmidlemwe  4451  sotri2  4892  poltletr  4895  funprg  5129  funtpg  5130  fntpg  5135  funimaexglem  5162  fvun1  5439  ftpg  5556  fsnunf  5572  fsnunfv  5573  caovimo  5916  brtposg  6103  smoel  6149  rdgivallem  6230  frecsuclem  6255  mapxpen  6693  unsnfi  6758  unsnfidcex  6759  unsnfidcel  6760  sbthlemi4  6798  elfir  6811  updjud  6917  ltsopi  7070  distrnqg  7137  ltmnqg  7151  mulcanenq0ec  7195  distrnq0  7209  prarloclem5  7250  1idprl  7340  1idpru  7341  ltaprg  7369  recexprlemopl  7375  recexprlemopu  7377  recexprlem1ssl  7383  aptipr  7391  ltmprr  7392  cauappcvgprlemlol  7397  cauappcvgprlemupu  7399  caucvgprlemlol  7420  caucvgprlemupu  7422  caucvgprprlemlol  7448  caucvgprprlemupu  7450  readdcan  7819  cnegexlem2  7855  addcan2  7860  ltadd2  8094  apreap  8261  ltmul1  8266  apcotr  8281  apadd1  8282  mulext1  8286  divdirap  8364  divcanap5  8381  ltdiv1  8530  lt2halves  8853  zdivmul  9039  eluzsub  9251  ledivge1le  9406  addlelt  9442  xaddass  9539  xleadd1  9545  xltadd1  9546  elioo5  9603  iccsupr  9636  iccneg  9659  icoshft  9660  icoshftf1o  9661  zltaddlt1le  9676  fzen  9710  elfz1b  9757  fzrevral  9772  fzshftral  9775  elfz0ubfz0  9789  elfz0fzfz0  9790  fz0fzelfz0  9791  fz0fzdiffz0  9794  elfzo  9813  fzodcel  9816  elfzonlteqm1  9874  modqaddmulmod  10051  expdivap  10231  leexp2a  10233  bcval3  10384  omgadd  10435  shftfibg  10479  elicc4abs  10752  xrmaxltsup  10913  xrmaxadd  10916  xrlemininf  10926  xrminltinf  10927  mulcn2  10967  fsumsplitsnun  11074  demoivreALT  11324  dvdsval2  11338  dvdsmulcr  11365  modmulconst  11367  dvdsexp  11401  oddge22np1  11420  modremain  11468  mulgcd  11544  mulgcdr  11546  gcddiv  11547  rpmulgcd  11554  rplpwr  11555  coprmdvds  11613  cncongr1  11624  dvdsnprmd  11646  prmexpb  11669  rpexp  11671  cncongrprm  11675  isstructr  11811  setsvala  11827  setsresg  11834  strle3g  11888  clsss  12124  ntrcls0  12137  neiss  12156  neipsm  12160  cnpnei  12224  cncnp2m  12236  cnconst2  12238  sslm  12252  upxp  12277  txmetcn  12502  findset  12826