Theorem biadanii 834

Description: Inference associated with biadani 832. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)

Hypotheses

Ref	Expression
biadani.1	⊢ (𝜑 → 𝜓)
biadanii.2	⊢ (𝜓 → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
biadanii	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Proof of Theorem biadanii

Step	Hyp	Ref	Expression
1		biadanii.2	. 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
2		biadani.1	. . 3 ⊢ (𝜑 → 𝜓)
3	2	biadani 832	. 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
4	1, 3	mpbi 233	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ 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:  elab4g  3637  elpwb  4565  ssdifsn  4751  brab2a  5748  elon2  6368  elovmpo  7660  eqop2  8030  iscard  9983  iscard2  9984  elnnnn0  12574  elfzo2  13720  bitsval  16517  1nprm  16772  funcpropd  17994  isfull  18004  isfth  18008  ismgmhm  18801  ismhm  18896  isghm  19346  ghmpropd  19386  isga  19421  oppgcntz  19494  gexdvdsi  19713  isrnghm  20585  isrhm  20623  issdrg  20957  abvpropd  21004  islmhm  21214  dfprm2  21689  prmirred  21690  elocv  21884  isobs  21936  iscn2  23466  iscnp2  23467  islocfin  23746  elflim2  24193  isfcls  24238  isnghm  24952  isnmhm  24975  0plef  25903  elply  26423  dchrelbas4  27482  brslts  28030  nb3grpr  29845  ispligb  30961  isph  31306  abfmpunirn  33128  iscvm  35841  sscoid  36493  bj-pwvrelb  37644  bj-elsnb  37808  bj-ideqb  37914  bj-opelidb1ALT  37921  bj-elid5  37924  eldiophb  43605  eldioph3b  43613  eldioph4b  43655  bropabg  44167  brfvrcld2  44535  islmd  50594  iscmd  50595