Theorem biantru 537

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
biantru.1	⊢ 𝜑

Assertion

Ref	Expression
biantru	⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

Proof of Theorem biantru

Step	Hyp	Ref	Expression
1		biantru.1	. 2 ⊢ 𝜑
2		iba 535	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 208   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  biantrur  538  pm4.71  565  eu6lem  2600  eu6  2601  issettru  2840  issetlem  2842  rextru  3093  rexcom4b  3485  eueq  3671  ssrabeq  4037  nsspssun  4220  disjpss  4415  reusngf  4633  reuprg0  4661  reuprg  4662  pr1eqbg  4815  disjprg  5096  ax6vsep  5253  pwun  5540  dfid3  5545  elvv  5722  elvvv  5723  dfres3  5970  resopab  6023  xpcan2  6163  funfn  6551  dffn2  6693  dffn3  6704  dffn4  6784  fsn  7117  sucexb  7787  fparlem1  8091  ixp0x  8908  ac6sfi  9228  fiint  9271  rankc1  9828  cf0  10207  ind1a  12206  ccatrcan  14732  prmreclem2  16953  subislly  23541  ovoliunlem1  25564  plyun0  26257  dmcuts  27884  rightge0  27914  tgjustf  28642  ercgrg  28686  dfpth2  29929  0wlk  30318  0trl  30324  0pth  30327  0cycl  30336  nmoolb  30974  hlimreui  31442  nmoplb  32110  nmfnlb  32127  dmdbr5ati  32625  disjunsn  32794  esplyind  33872  fsumcvg4  34247  issibf  34630  bnj1174  35298  derang0  35519  subfacp1lem6  35535  satfdm  35719  bj-denoteslem  37356  bj-rexcom4bv  37367  bj-rexcom4b  37368  bj-tagex  37472  bj-dfid2ALT  37550  bj-restuni  37587  rdgeqoa  37864  ftc1anclem5  38196  disjressuc2  38910  eqvrelcoss3  39201  dfeldisj5  39312  dibord  41783  eu6w  43258  ifpnot  44046  ifpdfxor  44063  ifpid1g  44070  ifpim1g  44077  ifpimimb  44080  relopabVD  45476  n0abso  45552  euabsneu  47622  rmotru  49424  reutru  49425