Theorem biantru 539

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biantrur  540  pm4.71  567  eu6lem  2603  eu6  2604  issettru  2843  issetlem  2845  rextru  3098  rexcom4b  3488  eueq  3673  ssrabeq  4039  nsspssun  4221  disjpss  4421  reusngf  4642  reuprg0  4670  reuprg  4671  pr1eqbg  4824  disjprg  5107  ax6vsep  5268  pwun  5556  dfid3  5561  elvv  5738  elvvv  5739  dfres3  5985  resopab  6038  xpcan2  6177  funfn  6570  dffn2  6711  dffn3  6722  dffn4  6802  fsn  7135  sucexb  7809  fparlem1  8113  ixp0x  8930  ac6sfi  9251  fiint  9293  rankc1  9849  cf0  10249  ind1a  12246  ccatrcan  14780  prmreclem2  17001  subislly  23691  ovoliunlem1  25714  plyun0  26407  dmcuts  28037  rightge0  28067  tgjustf  28795  ercgrg  28839  dfpth2  30143  0wlk  30536  0trl  30542  0pth  30545  0cycl  30554  nmoolb  31196  hlimreui  31664  nmoplb  32332  nmfnlb  32349  dmdbr5ati  32847  disjunsn  33012  esplyind  34031  fsumcvg4  34406  issibf  34790  bnj1174  35458  derang0  35700  subfacp1lem6  35716  satfdm  35900  bj-denoteslem  37565  bj-rexcom4bv  37576  bj-rexcom4b  37577  bj-tagex  37682  bj-dfid2ALT  37760  bj-restuni  37798  rdgeqoa  38075  ftc1anclem5  38407  disjressuc2  39120  eqvrelcoss3  39411  dfeldisj5  39522  dibord  41993  eu6w  43468  ifpnot  44256  ifpdfxor  44273  ifpid1g  44280  ifpim1g  44287  ifpimimb  44290  relopabVD  45669  n0abso  45745  euabsneu  47825  rmotru  49640  reutru  49641