Theorem biimprd 136

Description: Deduce a converse implication from a logical equivalence.

Hypothesis

Ref	Expression
biimpd.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
biimprd	⊢ (φ → (χ → ψ))

Proof of Theorem biimprd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		bi2 131	. 2 ⊢ ((ψ ↔ χ) → (χ → ψ))
3	1, 2	syl 12	1 ⊢ (φ → (χ → ψ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  biimprcd 138  mpbiri 169  mpbird 171  sylibrd 179  sylbird 180  syl5bir 184  syl6bir 188  biimpar 325  bitrd 406  anbi2d 468  mtbid 536  mtbii 538  del34b 837  a4w1 930  elab3g 1420  sspsstr 1575  so 2152  dfwe2 2187  wefrc 2195  ordsseleq 2227  oneqmini 2272  ordsucelsuc 2324  orduniorsuc 2337  ordzsl 2366  tfinds 2401  opelxpi 2455  2elresin 2733  fnex 2740  tz6.12c 2846 &nšsp;fveqres 2851  f1owe 2943  f1oweOLD 2944  tfrlem9 2957  tz7.48lem 2993  abianfp 3000  oprabval 3047  ndmordi 3065  oawordeulem 3156  nnacl 3172  f1oeng 3298  f1domg 3299  sbthlem1 3349  fiint 3445  inf3lem3 3466  trcl 3489  r1tr 3498  rankr1 3518  entri 3645  cardaleph 3690  indpi 3828  prlem934a 3931  addcanpr 3946  reclem3pr 3952  lelttrt 4289  add20 4329  nnmulclt 4437  arch 4521  nnnegz 4566  sqrlem6 4736  clim0 4882  hlim0 5140  projlem15 5207  spanun 5450  spansncol 5473  spansneleq 5475  spansnsst 5476  elspansn5t 5479  pjin 5584  pjnormss 5638  dmdbr 5731

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depend= on definitions:  df-bi 128

metamath.org