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  4440  fcofo  5907  acexmid  5999  rdgon  6530  oawordi  6613  nnmord  6661  nnmword  6662  fidifsnen  7028  dif1en  7037  ac6sfi  7056  difinfsn  7263  2omotaplemap  7439  enq0tr  7617  distrlem4prl  7767  distrlem4pru  7768  ltaprg  7802  lelttr  8231  ltletr  8232  readdcan  8282  addcan  8322  addcan2  8323  ltadd2  8562  divmulassap  8838  xrlelttr  9998  xrltletr  9999  xaddass  10061  xleadd1a  10065  xlesubadd  10075  icoshftf1o  10183  difelfzle  10326  fzo1fzo0n0  10379  modqmuladdim  10584  modqmuladdnn0  10585  modqm1p1mod0  10592  q2submod  10602  modifeq2int  10603  modqaddmulmod  10608  seq1g  10680  seqp1g  10683  ltexp2a  10808  exple1  10812  expnlbnd2  10882  nn0ltexp2  10926  nn0leexp2  10927  mulsubdivbinom2ap  10928  expcan  10933  fiprsshashgt1  11034  fun2dmnop0  11064  ccatass  11138  fzowrddc  11174  swrdclg  11177  ccatopth  11243  pfxccatin12lem2a  11254  pfxccat3  11261  maxleastb  11720  maxltsup  11724  xrltmaxsup  11763  xrmaxltsup  11764  xrmaxaddlem  11766  xrmaxadd  11767  addcn2  11816  mulcn2  11818  isumz  11895  dvdsmodexp  12301  modmulconst  12329  dvdsmod  12368  divalglemex  12428  divalg  12430  gcdass  12531  rplpwr  12543  rppwr  12544  nnwodc  12552  uzwodc  12553  rpmulgcd2  12612  rpdvds  12616  rpexp  12670  znege1  12695  prmdiveq  12753  hashgcdlem  12755  coprimeprodsq  12775  coprimeprodsq2  12776  pythagtriplem3  12785  pcdvdsb  12838  pcgcd1  12846  dvdsprmpweq  12853  pcbc  12869  ctinf  12996  nninfdc  13019  isnsgrp  13434  issubmnd  13470  mulgnn0p1  13665  mulgnnsubcl  13666  mulgneg  13672  mulgdirlem  13685  nmzsubg  13742  ghmmulg  13788  ring1eq0  14006  rmodislmod  14309  lspss  14357  2idlcpblrng  14481  neiint  14813  topssnei  14830  cnptopco  14890  cnrest2  14904  cnptoprest  14907  upxp  14940  bldisj  15069  blgt0  15070  bl2in  15071  blss2ps  15074  blss2  15075  xblm  15085  blssps  15095  blss  15096  bdmopn  15172  metcnp2  15181  txmetcnp  15186  cncfmptc  15264  dvcnp2cntop  15367  dvcn  15368  ply1term  15411  dvply1  15433  logdivlti  15549  ltexp2  15609  lgsfvalg  15678  lgsneg  15697  lgsmod  15699  lgsdilem  15700  lgsdirprm  15707  lgsdir  15708  lgsdi  15710  lgsne0  15711  1dom1el  16312