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  2601  eu6  2602  issettru  2841  issetlem  2843  rextru  3096  rexcom4b  3484  eueq  3668  ssrabeq  4011  nsspssun  4215  disjpss  4416  reusngf  4634  reuprg0  4662  reuprg  4663  pr1eqbg  4814  disjprg  5101  ax6vsep  5259  pwun  5547  dfid3  5552  elvvOLD  5730  elvvv  5731  dfres3  5979  resopab  6031  xpcan2  6174  funfn  6578  dffn2  6719  dffn3  6730  dffn4  6810  fsn  7144  sucexb  7825  fparlem1  8133  ixp0x  8965  ac6sfi  9286  fiint  9329  rankc1  9897  cf0  10338  ind1a  12341  ccatrcan  14879  prmreclem2  17107  subislly  23812  ovoliunlem1  25835  plyun0  26527  dmcuts  28189  rightge0  28219  tgjustf  28947  ercgrg  28992  dfpth2  30326  0wlk  30719  0trl  30725  0pth  30728  0cycl  30737  nmoolb  31385  hlimreui  31853  nmoplb  32521  nmfnlb  32538  dmdbr5ati  33036  disjunsn  33242  esplyind  34260  fsumcvg4  34635  issibf  35018  bnj1174  35686  derang0  36055  subfacp1lem6  36071  satfdm  36255  bj-denoteslem  37910  bj-rexcom4bv  37921  bj-rexcom4b  37922  bj-tagex  38027  bj-dfid2ALT  38119  bj-restuni  38157  rdgeqoa  38433  ftc1anclem5  38755  disjressuc2  39483  eqvrelcoss3  39774  dfeldisj5  39885  dibord  42356  eu6w  43827  ifpnot  44611  ifpdfxor  44628  ifpid1g  44635  ifpim1g  44642  ifpimimb  44645  relopabVD  46022  n0abso  46105  euabsneu  48237  rmotru  50052  reutru  50053