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  7440  2omotaplemap  7623  enq0tr  7801  distrlem4prl  7951  distrlem4pru  7952  ltaprg  7986  lelttr  8414  ltletr  8415  readdcan  8467  addcan  8507  addcan2  8508  ltadd2  8748  divmulassap  9027  indfdc  9300  xrlelttr  10218  xrltletr  10219  xaddass  10281  xleadd1a  10285  xlesubadd  10295  icoshftf1o  10403  lincmble  10416  difelfzle  10551  fzo1fzo0n0  10605  modqmuladdim  10817  modqmuladdnn0  10818  modqm1p1mod0  10825  q2submod  10835  modifeq2int  10836  modqaddmulmod  10841  seq1g  10913  seqp1g  10916  ltexp2a  11041  exple1  11045  expnlbnd2  11116  nn0ltexp2  11161  nn0leexp2  11162  mulsubdivbinom2ap  11163  expcan  11168  fiprsshashgt1  11272  hashtpgim  11311  hashtpg  11313  fun2dmnop0  11316  ccatass  11390  fzowrddc  11433  swrdclg  11436  ccatopth  11502  pfxccatin12lem2a  11513  pfxccat3  11520  maxleastb  11995  maxltsup  11999  xrltmaxsup  12039  xrmaxltsup  12040  xrmaxaddlem  12042  xrmaxadd  12043  addcn2  12092  mulcn2  12094  isumz  12172  dvdsmodexp  12578  modmulconst  12606  dvdsmod  12645  divalglemex  12705  divalg  12707  gcdass  12808  rplpwr  12820  rppwr  12821  nnwodc  12829  uzwodc  12830  rpmulgcd2  12889  rpdvds  12893  rpexp  12948  znege1  12974  prmdiveq  13034  hashgcdlem  13036  coprimeprodsq  13056  coprimeprodsq2  13057  pythagtriplem3  13066  pcdvdsb  13119  pcgcd1  13127  dvdsprmpweq  13134  pcbc  13150  ctinf  13370  nninfdc  13393  isnsgrp  13770  issubmnd  13804  mulgnn0p1  13985  mulgnnsubcl  13986  mulgneg  13992  mulgdirlem  14005  nmzsubg  14062  ghmmulg  14108  gsumsncmn  14205  ring1eq0  14402  rmodislmod  14737  lspss  14785  2idlcpblrng  14909  issubassa  15062  aspss  15068  neiint  15295  topssnei  15312  cnptopco  15372  cnrest2  15386  cnptoprest  15389  upxp  15422  bldisj  15551  blgt0  15552  bl2in  15553  blss2ps  15556  blss2  15557  xblm  15567  blssps  15577  blss  15578  bdmopn  15654  metcnp2  15663  txmetcnp  15668  cncfmptc  15746  dvcnp2cntop  15849  dvcn  15850  ply1term  15893  dvply1  15915  logdivlti  16033  ltexp2  16096  pellexlem2  16149  bcmono  16202  lgsfvalg  16222  lgsneg  16241  lgsmod  16243  lgsdilem  16244  lgsdirprm  16251  lgsdir  16252  lgsdi  16254  lgsne0  16255