Theorem biantru 538

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 536	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biantrur  539  pm4.71  566  eu6lem  2607  eu6  2608  issettru  2847  issetlem  2849  rextru  3102  rexcom4b  3494  eueq  3680  ssrabeq  4046  nsspssun  4229  disjpss  4427  reusngf  4645  reuprg0  4673  reuprg  4674  pr1eqbg  4826  disjprg  5109  ax6vsep  5268  pwun  5555  dfid3  5560  elvv  5737  elvvv  5738  dfres3  5984  resopab  6037  xpcan2  6176  funfn  6567  dffn2  6708  dffn3  6719  dffn4  6799  fsn  7132  sucexb  7803  fparlem1  8107  ixp0x  8924  ac6sfi  9244  fiint  9286  rankc1  9842  cf0  10234  ind1a  12229  ccatrcan  14756  prmreclem2  16977  subislly  23607  ovoliunlem1  25630  plyun0  26323  dmcuts  27950  rightge0  27980  tgjustf  28708  ercgrg  28752  dfpth2  30019  0wlk  30408  0trl  30414  0pth  30417  0cycl  30426  nmoolb  31064  hlimreui  31532  nmoplb  32200  nmfnlb  32217  dmdbr5ati  32715  disjunsn  32880  esplyind  33910  fsumcvg4  34285  issibf  34668  bnj1174  35336  derang0  35560  subfacp1lem6  35576  satfdm  35760  bj-denoteslem  37395  bj-rexcom4bv  37406  bj-rexcom4b  37407  bj-tagex  37511  bj-dfid2ALT  37589  bj-restuni  37627  rdgeqoa  37904  ftc1anclem5  38236  disjressuc2  38950  eqvrelcoss3  39241  dfeldisj5  39352  dibord  41823  eu6w  43300  ifpnot  44088  ifpdfxor  44105  ifpid1g  44112  ifpim1g  44119  ifpimimb  44122  relopabVD  45501  n0abso  45577  euabsneu  47654  rmotru  49466  reutru  49467