Theorem impbid1 515

Description: Infer an equivalence from two implications.

Hypotheses

Ref	Expression
impbid1.1	|- (ph -> (ps -> ch))
impbid1.2	|- (ch -> ps)

Assertion

Ref	Expression
impbid1	|- (ph -> (ps <-> ch))

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 |- (ph -> (ps -> ch))
2		impbid1.2	. . 3 |- (ch -> ps)
3	2	a1i 8	. 2 |- (ph -> (ch -> ps))
4	1, 3	impbid 514	1 |- (ph -> (ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  pm4.71 633  biantrud 724  bianfd 736  pm5.71 746  19.33b 1088  sb4b 1219  a16gb 1272  2eu1 1442  2eu3 1444  ceqsalg 1816  undif4 2315  opthpr 2476  elpwuni 2751  iunpw 2904  onint0 2997  ordssun 3069  suc11 3083  unizlim 3103  xp11 3463  imadif 3560  2elresin 3584  f1fveq 3861  oa00 4177  omcan 4184  oecan 4200  nnarcl 4216  nnaordex 4233  nnawordex 4234  erth 4266  fundmen 4409  0sdomg 4446  onfin 4499  unidom 4780  cardsdomel 4824  iscard2 4826  cardalephex 4858  cfeq0 4886  axrepnd 4918  cnegextlem1 5317  add20 5576  xrmaxltt 5861  xrltmint 5862  maxlet 5866  lemint 5869  maxltt 5870  xrub 6027  supxrre 6030  iooval2t 6304  uz11t 6364  fzoptht 6434  expeq0t 6517  expcant 6532  sq01t 6582  sqr11 6633  recant 6842  cau3 6853  infdif2 7512  infmap2lem2 7522  istps2 7549  tgval3t 7567  grprcan 7997  grplcan 8010  ip2eqi 8448  hial2eqt 8893  eigorth 9680  stge1 10075  stle0 10076  mdbr3 10134  mdbr4 10135  atsseq 10182  mdsymlem7 10244  oooeqim2 10371  hmeogrp 10425

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  df-an 225

Copyright terms: Public domain