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 )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

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 1011

This theorem is referenced by:  simpll3  1069  simprl3  1075  simp1l3  1123  simp2l3  1129  simp3l3  1135  3anandirs  1389  ifnetruedc  3681  frirrg  4490  fcofo  5980  acexmid  6074  rdgon  6647  oawordi  6732  nnmord  6780  nnmword  6781  1dom1el  7097  mapunen  7141  fidifsnen  7162  dif1en  7173  ac6sfi  7192  fissfi  7253  difinfsn  7430  2omotaplemap  7613  enq0tr  7791  distrlem4prl  7941  distrlem4pru  7942  ltaprg  7976  lelttr  8404  ltletr  8405  readdcan  8456  addcan  8496  addcan2  8497  ltadd2  8737  divmulassap  9015  xrlelttr  10187  xrltletr  10188  xaddass  10250  xleadd1a  10254  xlesubadd  10264  icoshftf1o  10372  lincmble  10385  difelfzle  10519  fzo1fzo0n0  10573  modqmuladdim  10782  modqmuladdnn0  10783  modqm1p1mod0  10790  q2submod  10800  modifeq2int  10801  modqaddmulmod  10806  seq1g  10878  seqp1g  10881  ltexp2a  11006  exple1  11010  expnlbnd2  11081  nn0ltexp2  11125  nn0leexp2  11126  mulsubdivbinom2ap  11127  expcan  11132  fiprsshashgt1  11236  hashtpgim  11275  hashtpg  11277  fun2dmnop0  11280  ccatass  11354  fzowrddc  11397  swrdclg  11400  ccatopth  11466  pfxccatin12lem2a  11477  pfxccat3  11484  maxleastb  11958  maxltsup  11962  xrltmaxsup  12001  xrmaxltsup  12002  xrmaxaddlem  12004  xrmaxadd  12005  addcn2  12054  mulcn2  12056  isumz  12134  dvdsmodexp  12540  modmulconst  12568  dvdsmod  12607  divalglemex  12667  divalg  12669  gcdass  12770  rplpwr  12782  rppwr  12783  nnwodc  12791  uzwodc  12792  rpmulgcd2  12851  rpdvds  12855  rpexp  12909  znege1  12934  prmdiveq  12992  hashgcdlem  12994  coprimeprodsq  13014  coprimeprodsq2  13015  pythagtriplem3  13024  pcdvdsb  13077  pcgcd1  13085  dvdsprmpweq  13092  pcbc  13108  ctinf  13299  nninfdc  13322  isnsgrp  13698  issubmnd  13732  mulgnn0p1  13913  mulgnnsubcl  13914  mulgneg  13920  mulgdirlem  13933  nmzsubg  13990  ghmmulg  14036  gsumsncmn  14133  ring1eq0  14326  rmodislmod  14660  lspss  14708  2idlcpblrng  14832  neiint  15169  topssnei  15186  cnptopco  15246  cnrest2  15260  cnptoprest  15263  upxp  15296  bldisj  15425  blgt0  15426  bl2in  15427  blss2ps  15430  blss2  15431  xblm  15441  blssps  15451  blss  15452  bdmopn  15528  metcnp2  15537  txmetcnp  15542  cncfmptc  15620  dvcnp2cntop  15723  dvcn  15724  ply1term  15767  dvply1  15789  logdivlti  15905  ltexp2  15966  pellexlem2  16006  lgsfvalg  16038  lgsneg  16057  lgsmod  16059  lgsdilem  16060  lgsdirprm  16067  lgsdir  16068  lgsdi  16070  lgsne0  16071