Theorem simpl3 1033

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

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

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 1030	. 2 |- ( ( ph /\ ps /\ ch ) -> ch )
2	1	adantr 276	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll3  1069  simprl3  1075  simp1l3  1123  simp2l3  1129  simp3l3  1135  3anandirs  1389  ifnetruedc  3684  frirrg  4497  fcofo  5993  acexmid  6087  rdgon  6661  oawordi  6746  nnmord  6794  nnmword  6795  1dom1el  7111  mapunen  7155  fidifsnen  7176  dif1en  7187  ac6sfi  7206  fissfi  7267  difinfsn  7446  2omotaplemap  7629  enq0tr  7807  distrlem4prl  7957  distrlem4pru  7958  ltaprg  7992  lelttr  8420  ltletr  8421  readdcan  8473  addcan  8513  addcan2  8514  ltadd2  8754  divmulassap  9033  indfdc  9307  xrlelttr  10225  xrltletr  10226  xaddass  10288  xleadd1a  10292  xlesubadd  10302  icoshftf1o  10410  lincmble  10423  difelfzle  10558  fzo1fzo0n0  10612  modqmuladdim  10825  modqmuladdnn0  10826  modqm1p1mod0  10833  q2submod  10843  modifeq2int  10844  modqaddmulmod  10849  seq1g  10921  seqp1g  10924  ltexp2a  11049  exple1  11053  expnlbnd2  11124  nn0ltexp2  11169  nn0leexp2  11170  mulsubdivbinom2ap  11171  expcan  11176  fiprsshashgt1  11280  hashtpgim  11319  hashtpg  11321  fun2dmnop0  11324  ccatass  11398  fzowrddc  11441  swrdclg  11444  ccatopth  11510  pfxccatin12lem2a  11521  pfxccat3  11528  maxleastb  12003  maxltsup  12007  xrltmaxsup  12048  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  addcn2  12101  mulcn2  12103  isumz  12181  dvdsmodexp  12587  modmulconst  12615  dvdsmod  12654  divalglemex  12714  divalg  12716  gcdass  12817  rplpwr  12829  rppwr  12830  nnwodc  12838  uzwodc  12839  rpmulgcd2  12898  rpdvds  12902  rpexp  12957  znege1  12983  prmdiveq  13043  hashgcdlem  13045  coprimeprodsq  13065  coprimeprodsq2  13066  pythagtriplem3  13075  pcdvdsb  13128  pcgcd1  13136  dvdsprmpweq  13143  pcbc  13159  ctinf  13379  nninfdc  13402  isnsgrp  13780  issubmnd  13814  mulgnn0p1  13995  mulgnnsubcl  13996  mulgneg  14002  mulgdirlem  14015  nmzsubg  14072  ghmmulg  14118  gsumsncmn  14246  ring1eq0  14460  rmodislmod  14797  lspss  14845  2idlcpblrng  14969  issubassa  15122  aspss  15128  neiint  15371  topssnei  15388  cnptopco  15448  cnrest2  15462  cnptoprest  15465  upxp  15498  bldisj  15627  blgt0  15628  bl2in  15629  blss2ps  15632  blss2  15633  xblm  15643  blssps  15653  blss  15654  bdmopn  15730  metcnp2  15739  txmetcnp  15744  cncfmptc  15822  dvcnp2cntop  15925  dvcn  15926  ply1term  15969  dvply1  15991  logdivlti  16111  ltexp2  16177  pellexlem2  16230  bcmono  16304  lgsfvalg  16329  lgsneg  16348  lgsmod  16350  lgsdilem  16351  lgsdirprm  16358  lgsdir  16359  lgsdi  16361  lgsne0  16362