Theorem biadanii 819

Description: Inference associated with biadani 817. 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 817	. 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
4	1, 3	mpbi 229	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  elab4g  3614  elpwb  4543  ssdifsn  4721  brab2a  5680  elon2  6277  elovmpo  7514  eqop2  7874  iscard  9733  iscard2  9734  elnnnn0  12276  elfzo2  13390  bitsval  16131  1nprm  16384  funcpropd  17616  isfull  17626  isfth  17630  ismhm  18432  isghm  18834  ghmpropd  18872  isga  18897  oppgcntz  18971  gexdvdsi  19188  isrhm  19965  issdrg  20063  abvpropd  20102  islmhm  20289  dfprm2  20695  prmirred  20696  elocv  20873  isobs  20927  iscn2  22389  iscnp2  22390  islocfin  22668  elflim2  23115  isfcls  23160  isnghm  23887  isnmhm  23910  0plef  24836  elply  25356  dchrelbas4  26391  nb3grpr  27749  ispligb  28839  isph  29184  abfmpunirn  30989  iscvm  33221  brsslt  33980  sscoid  34215  bj-pwvrelb  35083  bj-elsnb  35232  bj-ideqb  35330  bj-opelidb1ALT  35337  bj-elid5  35340  eldiophb  40579  eldioph3b  40587  eldioph4b  40633  brfvrcld2  41300  ismgmhm  45337  isrnghm  45450