Theorem biimprcd 156

Description: Deduce a converse commuted implication from a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem biimprcd

Step	Hyp	Ref	Expression
1		biimpd.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	biimprd 154	. 2 ⊢ (φ → (χ → ψ))
3	2	com12 11	1 ⊢ (χ → (φ → ψ))

Syntax hints:   → wi 3   ↔ wb 146

This theorem is referenced by:  biimparc 421  prlem1 774  ax11i 1142  ax11eq 1367  ax11el 1368  eleq1a 1550  ceqsalg 1832  cgsexg 1838  cgsex2g 1839  cgsex4g 1840  ceqsex 1841  cla42egv 1871  cla43egv 1873  ralxfr 2915  iunpw 2930  onfr 3002  ordun 3097  funcnvuni 3580  funfvop 3819  cbvfo 3901  abianfp 3978  oaordex 4208  ecelqsi 4310  eceqopreq 4331  fundmen 4446  nneneq 4532  unfilem1 4566  ac6lem 4771  zorn2lem3 4807  zorn2lem7 4811  ltrpq 5105  genpnnp 5128  ltaddpr 5160  reclem3pr 5178  reclem4pr 5179  suppsrlem 5241  suppsr3 5244  suprelem 5279  elfz4 6443  abslti 6907  abslei 6908  cau2i 6945  fsum1i 7037  ser1clim0 7205  unctb 7610  cnsscnp 7798  nmoubi 8460  nmopub 9856  nmfnleub 9873  mdbr3 10249  mdbr4 10250  atssma 10330  atcvatlem 10337  uninqs 10466  hmphre 10563  iintlem1 10653  mrdmcd 10743

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain