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

Theorem biantrurd 303
 Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
biantrud.1 (𝜑𝜓)
Assertion
Ref Expression
biantrurd (𝜑 → (𝜒 ↔ (𝜓𝜒)))

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2 (𝜑𝜓)
2 ibar 299 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 14 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  mpbirand  437  3anibar  1149  drex1  1770  elrab3t  2839  bnd2  4097  opbrop  4618  opelresi  4830  funcnv3  5185  fnssresb  5235  dff1o5  5376  fneqeql2  5529  fnniniseg2  5543  rexsupp  5544  dffo3  5567  fmptco  5586  fnressn  5606  fconst4m  5640  riota2df  5750  eloprabga  5858  frecabcl  6296  mptelixpg  6628  exmidfodomrlemreseldju  7056  enq0breq  7251  genpassl  7339  genpassu  7340  elnnnn0  9027  peano2z  9097  znnsub  9112  znn0sub  9126  uzin  9365  nn01to3  9416  rpnegap  9481  negelrp  9482  xsubge0  9671  divelunit  9792  elfz5  9805  uzsplit  9879  elfzonelfzo  10014  adddivflid  10072  divfl0  10076  2shfti  10610  rexuz3  10769  clim2c  11060  fisumss  11168  infssuzex  11649  bezoutlemmain  11693  eltg3  12236  lmbrf  12394  cnrest2  12415  cnptoprest  12418  cnptoprest2  12419  ismet2  12533  elbl2ps  12571  elbl2  12572  xblpnfps  12577  xblpnf  12578  bdxmet  12680  metcn  12693  cnbl0  12713  cnblcld  12714  mulc1cncf  12755  ellimc3apf  12808  pilem1  12873
 Copyright terms: Public domain W3C validator