Theorem simpl3 1026

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 1023	. 2 |- ( ( ph /\ ps /\ ch ) -> ch )
2	1	adantr 276	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )

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

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 1004

This theorem is referenced by:  simpll3  1062  simprl3  1068  simp1l3  1116  simp2l3  1122  simp3l3  1128  3anandirs  1382  ifnetruedc  3646  frirrg  4441  fcofo  5908  acexmid  6000  rdgon  6532  oawordi  6615  nnmord  6663  nnmword  6664  fidifsnen  7032  dif1en  7041  ac6sfi  7060  difinfsn  7267  2omotaplemap  7443  enq0tr  7621  distrlem4prl  7771  distrlem4pru  7772  ltaprg  7806  lelttr  8235  ltletr  8236  readdcan  8286  addcan  8326  addcan2  8327  ltadd2  8566  divmulassap  8842  xrlelttr  10002  xrltletr  10003  xaddass  10065  xleadd1a  10069  xlesubadd  10079  icoshftf1o  10187  difelfzle  10330  fzo1fzo0n0  10383  modqmuladdim  10589  modqmuladdnn0  10590  modqm1p1mod0  10597  q2submod  10607  modifeq2int  10608  modqaddmulmod  10613  seq1g  10685  seqp1g  10688  ltexp2a  10813  exple1  10817  expnlbnd2  10887  nn0ltexp2  10931  nn0leexp2  10932  mulsubdivbinom2ap  10933  expcan  10938  fiprsshashgt1  11039  fun2dmnop0  11069  ccatass  11143  fzowrddc  11179  swrdclg  11182  ccatopth  11248  pfxccatin12lem2a  11259  pfxccat3  11266  maxleastb  11725  maxltsup  11729  xrltmaxsup  11768  xrmaxltsup  11769  xrmaxaddlem  11771  xrmaxadd  11772  addcn2  11821  mulcn2  11823  isumz  11900  dvdsmodexp  12306  modmulconst  12334  dvdsmod  12373  divalglemex  12433  divalg  12435  gcdass  12536  rplpwr  12548  rppwr  12549  nnwodc  12557  uzwodc  12558  rpmulgcd2  12617  rpdvds  12621  rpexp  12675  znege1  12700  prmdiveq  12758  hashgcdlem  12760  coprimeprodsq  12780  coprimeprodsq2  12781  pythagtriplem3  12790  pcdvdsb  12843  pcgcd1  12851  dvdsprmpweq  12858  pcbc  12874  ctinf  13001  nninfdc  13024  isnsgrp  13439  issubmnd  13475  mulgnn0p1  13670  mulgnnsubcl  13671  mulgneg  13677  mulgdirlem  13690  nmzsubg  13747  ghmmulg  13793  ring1eq0  14011  rmodislmod  14315  lspss  14363  2idlcpblrng  14487  neiint  14819  topssnei  14836  cnptopco  14896  cnrest2  14910  cnptoprest  14913  upxp  14946  bldisj  15075  blgt0  15076  bl2in  15077  blss2ps  15080  blss2  15081  xblm  15091  blssps  15101  blss  15102  bdmopn  15178  metcnp2  15187  txmetcnp  15192  cncfmptc  15270  dvcnp2cntop  15373  dvcn  15374  ply1term  15417  dvply1  15439  logdivlti  15555  ltexp2  15615  lgsfvalg  15684  lgsneg  15703  lgsmod  15705  lgsdilem  15706  lgsdirprm  15713  lgsdir  15714  lgsdi  15716  lgsne0  15717  1dom1el  16354