ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpl3 GIF version

Theorem simpl3 969
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl3 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 966 . 2 ((𝜑𝜓𝜒) → 𝜒)
21adantr 272 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  simpll3  1005  simprl3  1011  simp1l3  1059  simp2l3  1065  simp3l3  1071  3anandirs  1309  frirrg  4240  fcofo  5651  acexmid  5739  rdgon  6249  oawordi  6331  nnmord  6379  nnmword  6380  fidifsnen  6730  dif1en  6739  ac6sfi  6758  difinfsn  6951  enq0tr  7206  distrlem4prl  7356  distrlem4pru  7357  ltaprg  7391  lelttr  7816  ltletr  7817  readdcan  7866  addcan  7906  addcan2  7907  ltadd2  8145  divmulassap  8415  xrlelttr  9529  xrltletr  9530  xaddass  9592  xleadd1a  9596  xlesubadd  9606  icoshftf1o  9714  difelfzle  9851  fzo1fzo0n0  9900  modqmuladdim  10080  modqmuladdnn0  10081  modqm1p1mod0  10088  q2submod  10098  modifeq2int  10099  modqaddmulmod  10104  ltexp2a  10285  exple1  10289  expnlbnd2  10357  expcan  10403  fiprsshashgt1  10503  maxleastb  10926  maxltsup  10930  xrltmaxsup  10966  xrmaxltsup  10967  xrmaxaddlem  10969  xrmaxadd  10970  addcn2  11019  mulcn2  11021  isumz  11098  modmulconst  11421  dvdsmod  11456  divalglemex  11515  divalg  11517  gcdass  11599  rplpwr  11611  rppwr  11612  rpmulgcd2  11672  rpdvds  11676  rpexp  11727  znege1  11751  hashgcdlem  11798  ctinf  11838  neiint  12209  topssnei  12226  cnptopco  12286  cnrest2  12300  cnptoprest  12303  upxp  12336  bldisj  12465  blgt0  12466  bl2in  12467  blss2ps  12470  blss2  12471  xblm  12481  blssps  12491  blss  12492  bdmopn  12568  metcnp2  12577  txmetcnp  12582  cncfmptc  12646  dvcnp2cntop  12706  dvcn  12707
  Copyright terms: Public domain W3C validator