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

Theorem biantrurd 299
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 295 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 14 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3anibar  1111  drex1  1726  elrab3t  2768  bnd2  4000  opbrop  4505  opelresi  4712  funcnv3  5062  fnssresb  5112  dff1o5  5246  fneqeql2  5392  fnniniseg2  5406  rexsupp  5407  dffo3  5430  fmptco  5448  fnressn  5467  fconst4m  5499  riota2df  5610  eloprabga  5717  frecabcl  6146  exmidfodomrlemreseldju  6805  enq0breq  6974  genpassl  7062  genpassu  7063  elnnnn0  8686  peano2z  8756  znnsub  8771  znn0sub  8785  uzin  9020  nn01to3  9071  rpnegap  9135  divelunit  9388  elfz5  9401  uzsplit  9473  elfzonelfzo  9606  adddivflid  9664  divfl0  9668  2shfti  10230  rexuz3  10388  clim2c  10636  fisumss  10748  infssuzex  11027  bezoutlemmain  11069
  Copyright terms: Public domain W3C validator