Theorem 3ad2ant3 1020

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

Syntax hints:   -> wi 4   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simp3l  1025  simp3r  1026  simp31  1033  simp32  1034  simp33  1035  simp3ll  1068  simp3lr  1069  simp3rl  1070  simp3rr  1071  simp3l1  1102  simp3l2  1103  simp3l3  1104  simp3r1  1105  simp3r2  1106  simp3r3  1107  simp31l  1120  simp31r  1121  simp32l  1122  simp32r  1123  simp33l  1124  simp33r  1125  simp311  1144  simp312  1145  simp313  1146  simp321  1147  simp322  1148  simp323  1149  simp331  1150  simp332  1151  simp333  1152  3anim123i  1184  3jaao  1308  ceqsalt  2763  ceqsralt  2764  vtoclgft  2787  ifbothdc  3567  tpssi  3759  sotricim  4323  elirr  4540  en2lp  4553  reg3exmidlemwe  4578  sotri2  5026  poltletr  5029  funprg  5266  funtpg  5267  fntpg  5272  funimaexglem  5299  fvun1  5582  ftpg  5700  fsnunf  5716  fsnunfv  5717  caovimo  6067  brtposg  6254  smoel  6300  rdgivallem  6381  frecsuclem  6406  mapxpen  6847  unsnfi  6917  unsnfidcex  6918  unsnfidcel  6919  sbthlemi4  6958  elfir  6971  updjud  7080  ltsopi  7318  distrnqg  7385  ltmnqg  7399  mulcanenq0ec  7443  distrnq0  7457  prarloclem5  7498  1idprl  7588  1idpru  7589  ltaprg  7617  recexprlemopl  7623  recexprlemopu  7625  recexprlem1ssl  7631  aptipr  7639  ltmprr  7640  cauappcvgprlemlol  7645  cauappcvgprlemupu  7647  caucvgprlemlol  7668  caucvgprlemupu  7670  caucvgprprlemlol  7696  caucvgprprlemupu  7698  readdcan  8096  cnegexlem2  8132  addcan2  8137  ltadd2  8375  apreap  8543  ltmul1  8548  apcotr  8563  apadd1  8564  mulext1  8568  divdirap  8653  divcanap5  8670  ltdiv1  8824  lt2halves  9153  zdivmul  9342  eluzsub  9556  ledivge1le  9725  addlelt  9767  xaddass  9868  xleadd1  9874  xltadd1  9875  elioo5  9932  iccsupr  9965  iccneg  9988  icoshft  9989  icoshftf1o  9990  zltaddlt1le  10006  fzen  10042  elfz1b  10089  fzrevral  10104  fzshftral  10107  elfz0ubfz0  10124  elfz0fzfz0  10125  fz0fzelfz0  10126  fz0fzdiffz0  10129  elfzo  10148  fzodcel  10151  elfzonlteqm1  10209  modqaddmulmod  10390  expdivap  10570  leexp2a  10572  bcval3  10730  omgadd  10781  shftfibg  10828  elicc4abs  11102  xrmaxltsup  11265  xrmaxadd  11268  xrlemininf  11278  xrminltinf  11279  mulcn2  11319  fsumsplitsnun  11426  prodfrecap  11553  demoivreALT  11780  dvdsval2  11796  dvdsmodexp  11801  dvdsmulcr  11827  modmulconst  11829  dvdsexp  11866  oddge22np1  11885  modremain  11933  mulgcd  12016  mulgcdr  12018  gcddiv  12019  rpmulgcd  12026  rplpwr  12027  coprmdvds  12091  cncongr1  12102  dvdsnprmd  12124  prmexpb  12150  rpexp  12152  cncongrprm  12156  modprm0  12253  modprmn0modprm0  12255  coprimeprodsq  12256  pythagtriplem1  12264  pythagtriplem3  12266  pythagtriplem10  12268  pythagtriplem6  12269  pythagtriplem11  12273  pythagtriplem12  12274  pythagtriplem13  12275  pythagtriplem15  12277  pythagtriplem17  12279  pythagtriplem19  12281  pcdvdsb  12318  dvdsprmpweqle  12335  pcfaclem  12346  isstructr  12476  setsvala  12492  setsresg  12499  strle3g  12566  imasaddvallemg  12735  fvprif  12761  mgmsscl  12779  insubm  12871  dfgrp3mlem  12967  mulgdirlem  13012  mulgp1  13014  mulgmodid  13020  eqglact  13082  clsss  13588  ntrcls0  13601  neiss  13620  neipsm  13624  cnpnei  13689  cncnp2m  13701  cnconst2  13703  sslm  13717  upxp  13742  txmetcn  13989  ptolemy  14215  sincosq1eq  14230  rplogbval  14333  rpcxplogb  14352  lgsdirprm  14405  lgsdirnn0  14418  2lgsoddprmlem1  14423  2lgsoddprmlem2  14424  findset  14667