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  2598  eu6  2599  issettru  2838  issetlem  2840  rextru  3093  rexcom4b  3481  eueq  3666  ssrabeq  4032  nsspssun  4214  disjpss  4414  reusngf  4635  reuprg0  4663  reuprg  4664  pr1eqbg  4817  disjprg  5099  ax6vsep  5260  pwun  5548  dfid3  5553  elvv  5730  elvvv  5731  dfres3  5977  resopab  6030  xpcan2  6170  funfn  6564  dffn2  6705  dffn3  6716  dffn4  6796  fsn  7130  sucexb  7804  fparlem1  8110  ixp0x  8936  ac6sfi  9257  fiint  9299  rankc1  9855  cf0  10255  ind1a  12256  ccatrcan  14791  prmreclem2  17012  subislly  23710  ovoliunlem1  25733  plyun0  26425  dmcuts  28059  rightge0  28089  tgjustf  28817  ercgrg  28862  dfpth2  30196  0wlk  30589  0trl  30595  0pth  30598  0cycl  30607  nmoolb  31255  hlimreui  31723  nmoplb  32391  nmfnlb  32408  dmdbr5ati  32906  disjunsn  33070  esplyind  34088  fsumcvg4  34463  issibf  34847  bnj1174  35515  derang0  35751  subfacp1lem6  35767  satfdm  35951  bj-denoteslem  37617  bj-rexcom4bv  37628  bj-rexcom4b  37629  bj-tagex  37734  bj-dfid2ALT  37812  bj-restuni  37850  rdgeqoa  38127  ftc1anclem5  38449  disjressuc2  39162  eqvrelcoss3  39453  dfeldisj5  39564  dibord  42035  eu6w  43525  ifpnot  44313  ifpdfxor  44330  ifpid1g  44337  ifpim1g  44344  ifpimimb  44347  relopabVD  45726  n0abso  45802  euabsneu  47919  rmotru  49734  reutru  49735