Theorem 3ad2ant2 1009

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantr 274	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant1 1005	1 |- ( ( ps /\ ph /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 968

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

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

This theorem is referenced by:  simp2l  1013  simp2r  1014  simp21  1020  simp22  1021  simp23  1022  simp2ll  1054  simp2lr  1055  simp2rl  1056  simp2rr  1057  simp2l1  1086  simp2l2  1087  simp2l3  1088  simp2r1  1089  simp2r2  1090  simp2r3  1091  simp21l  1104  simp21r  1105  simp22l  1106  simp22r  1107  simp23l  1108  simp23r  1109  simp211  1125  simp212  1126  simp213  1127  simp221  1128  simp222  1129  simp223  1130  simp231  1131  simp232  1132  simp233  1133  3anim123i  1174  3jaao  1298  ceqsalt  2751  vtoclgft  2775  vtoclegft  2797  ifbothdc  3551  frirrg  4327  elirr  4517  en2lp  4530  reg3exmidlemwe  4555  sotri3  5001  funtpg  5238  fnprg  5242  fntpg  5243  funimaexglem  5270  fnco  5295  fvun1  5551  oprssov  5979  caovimo  6031  rdgivallem  6345  fnsnsplitdc  6469  funresdfunsndc  6470  f1dom2g  6718  mapxpen  6810  ssfidc  6896  sbthlemi4  6921  ordiso2  6996  updjud  7043  difinfsn  7061  mkvprop  7118  endjudisj  7162  distrnqg  7324  distrnq0  7396  prarloclem5  7437  cauappcvgprlemlol  7584  cauappcvgprlemupu  7586  caucvgprlemlol  7607  caucvgprlemupu  7609  caucvgprprlemlol  7635  caucvgprprlemupu  7637  cnegexlem2  8070  apcotr  8501  apadd1  8502  mulext1  8506  div2negap  8627  ltdiv2  8778  nndivtr  8895  difgtsumgt  9256  zdivmul  9277  gtndiv  9282  fzind  9302  eluzuzle  9470  eluzp1p1  9487  peano2uz  9517  qdivcl  9577  irrmul  9581  ledivge1le  9658  xrre2  9753  xaddass  9801  xltadd1  9808  xlt2add  9812  ubioc1  9861  ubicc2  9917  zltaddlt1le  9939  uzsubsubfz  9978  elfz1b  10021  fzp1nel  10035  fz0fzdiffz0  10061  difelfzle  10065  elfzo0  10113  elfzonlteqm1  10141  fzonn0p1p1  10144  fzosplitprm1  10165  fzoshftral  10169  subfzo0  10173  ceiqle  10244  modqval  10255  modqvalr  10256  flqpmodeq  10258  modq0  10260  mulqmod0  10261  negqmod0  10262  modqge0  10263  modqlt  10264  modqelico  10265  modqdiffl  10266  modqmulnn  10273  modqvalp1  10274  modqmuladdnn0  10299  qnegmod  10300  addmodid  10303  q2submod  10316  modifeq2int  10317  modfzo0difsn  10326  addmodlteq  10329  omgadd  10711  hashun  10714  redivap  10812  imdivap  10819  xrmaxltsup  11195  xrmaxadd  11198  xrlemininf  11208  xrminltinf  11209  climuni  11230  mulcn2  11249  fsumsplitsnun  11356  prodfap0  11482  fprodabs  11553  efsub  11618  cos12dec  11704  dvdsmodexp  11731  summodnegmod  11758  divalglemex  11855  divalg  11857  modremain  11862  ndvdssub  11863  fldivndvdslt  11868  nndvdslegcd  11894  dfgcd2  11943  mulgcd  11945  mulgcdr  11947  gcddiv  11948  rplpwr  11956  rppwr  11957  qredeq  12024  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  pw2dvdslemn  12093  hashgcdlem  12166  modprm0  12182  modprmn0modprm0  12184  pythagtriplem1  12193  pythagtriplem3  12195  pythagtriplem10  12197  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem11  12202  pythagtriplem12  12203  pythagtriplem13  12204  pythagtriplem14  12205  pythagtriplem19  12210  pythagtrip  12211  dvdsprmpweqnn  12263  difsqpwdvds  12265  pcfaclem  12275  pcbc  12277  unennn  12326  ntrin  12724  elnei  12752  restco  12774  cnpnei  12819  cncnp2m  12831  sslm  12847  upxp  12872  blres  13034  metcnp3  13111  tgqioo  13147  ptolemy  13345  cxpcom  13457  logbgcd1irr  13485  logbprmirr  13490  lgslem1  13501  lgsneg  13525  lgsdilem  13528  lgsdir  13536  lgssq2  13542  lgsdirnn0  13548