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  4495  fcofo  5990  acexmid  6084  rdgon  6657  oawordi  6742  nnmord  6790  nnmword  6791  1dom1el  7107  mapunen  7151  fidifsnen  7172  dif1en  7183  ac6sfi  7202  fissfi  7263  difinfsn  7441  2omotaplemap  7624  enq0tr  7802  distrlem4prl  7952  distrlem4pru  7953  ltaprg  7987  lelttr  8415  ltletr  8416  readdcan  8468  addcan  8508  addcan2  8509  ltadd2  8749  divmulassap  9028  indfdc  9301  xrlelttr  10219  xrltletr  10220  xaddass  10282  xleadd1a  10286  xlesubadd  10296  icoshftf1o  10404  lincmble  10417  difelfzle  10552  fzo1fzo0n0  10606  modqmuladdim  10819  modqmuladdnn0  10820  modqm1p1mod0  10827  q2submod  10837  modifeq2int  10838  modqaddmulmod  10843  seq1g  10915  seqp1g  10918  ltexp2a  11043  exple1  11047  expnlbnd2  11118  nn0ltexp2  11163  nn0leexp2  11164  mulsubdivbinom2ap  11165  expcan  11170  fiprsshashgt1  11274  hashtpgim  11313  hashtpg  11315  fun2dmnop0  11318  ccatass  11392  fzowrddc  11435  swrdclg  11438  ccatopth  11504  pfxccatin12lem2a  11515  pfxccat3  11522  maxleastb  11997  maxltsup  12001  xrltmaxsup  12042  xrmaxltsup  12043  xrmaxaddlem  12045  xrmaxadd  12046  addcn2  12095  mulcn2  12097  isumz  12175  dvdsmodexp  12581  modmulconst  12609  dvdsmod  12648  divalglemex  12708  divalg  12710  gcdass  12811  rplpwr  12823  rppwr  12824  nnwodc  12832  uzwodc  12833  rpmulgcd2  12892  rpdvds  12896  rpexp  12951  znege1  12977  prmdiveq  13037  hashgcdlem  13039  coprimeprodsq  13059  coprimeprodsq2  13060  pythagtriplem3  13069  pcdvdsb  13122  pcgcd1  13130  dvdsprmpweq  13137  pcbc  13153  ctinf  13373  nninfdc  13396  isnsgrp  13774  issubmnd  13808  mulgnn0p1  13989  mulgnnsubcl  13990  mulgneg  13996  mulgdirlem  14009  nmzsubg  14066  ghmmulg  14112  gsumsncmn  14240  ring1eq0  14437  rmodislmod  14772  lspss  14820  2idlcpblrng  14944  issubassa  15097  aspss  15103  neiint  15337  topssnei  15354  cnptopco  15414  cnrest2  15428  cnptoprest  15431  upxp  15464  bldisj  15593  blgt0  15594  bl2in  15595  blss2ps  15598  blss2  15599  xblm  15609  blssps  15619  blss  15620  bdmopn  15696  metcnp2  15705  txmetcnp  15710  cncfmptc  15788  dvcnp2cntop  15891  dvcn  15892  ply1term  15935  dvply1  15957  logdivlti  16075  ltexp2  16138  pellexlem2  16191  bcmono  16265  lgsfvalg  16290  lgsneg  16309  lgsmod  16311  lgsdilem  16312  lgsdirprm  16319  lgsdir  16320  lgsdi  16322  lgsne0  16323