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  8466  addcan  8506  addcan2  8507  ltadd2  8747  divmulassap  9025  indfdc  9298  xrlelttr  10208  xrltletr  10209  xaddass  10271  xleadd1a  10275  xlesubadd  10285  icoshftf1o  10393  lincmble  10406  difelfzle  10541  fzo1fzo0n0  10595  modqmuladdim  10804  modqmuladdnn0  10805  modqm1p1mod0  10812  q2submod  10822  modifeq2int  10823  modqaddmulmod  10828  seq1g  10900  seqp1g  10903  ltexp2a  11028  exple1  11032  expnlbnd2  11103  nn0ltexp2  11147  nn0leexp2  11148  mulsubdivbinom2ap  11149  expcan  11154  fiprsshashgt1  11258  hashtpgim  11297  hashtpg  11299  fun2dmnop0  11302  ccatass  11376  fzowrddc  11419  swrdclg  11422  ccatopth  11488  pfxccatin12lem2a  11499  pfxccat3  11506  maxleastb  11980  maxltsup  11984  xrltmaxsup  12023  xrmaxltsup  12024  xrmaxaddlem  12026  xrmaxadd  12027  addcn2  12076  mulcn2  12078  isumz  12156  dvdsmodexp  12562  modmulconst  12590  dvdsmod  12629  divalglemex  12689  divalg  12691  gcdass  12792  rplpwr  12804  rppwr  12805  nnwodc  12813  uzwodc  12814  rpmulgcd2  12873  rpdvds  12877  rpexp  12931  znege1  12956  prmdiveq  13014  hashgcdlem  13016  coprimeprodsq  13036  coprimeprodsq2  13037  pythagtriplem3  13046  pcdvdsb  13099  pcgcd1  13107  dvdsprmpweq  13114  pcbc  13130  ctinf  13321  nninfdc  13344  isnsgrp  13721  issubmnd  13755  mulgnn0p1  13936  mulgnnsubcl  13937  mulgneg  13943  mulgdirlem  13956  nmzsubg  14013  ghmmulg  14059  gsumsncmn  14156  ring1eq0  14353  rmodislmod  14688  lspss  14736  2idlcpblrng  14860  issubassa  15013  aspss  15019  neiint  15246  topssnei  15263  cnptopco  15323  cnrest2  15337  cnptoprest  15340  upxp  15373  bldisj  15502  blgt0  15503  bl2in  15504  blss2ps  15507  blss2  15508  xblm  15518  blssps  15528  blss  15529  bdmopn  15605  metcnp2  15614  txmetcnp  15619  cncfmptc  15697  dvcnp2cntop  15800  dvcn  15801  ply1term  15844  dvply1  15866  logdivlti  15982  ltexp2  16043  pellexlem2  16092  lgsfvalg  16124  lgsneg  16143  lgsmod  16145  lgsdilem  16146  lgsdirprm  16153  lgsdir  16154  lgsdi  16156  lgsne0  16157