Theorem impbid1 519

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 518	1 |- (ph -> (ps <-> ch))

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

This theorem is referenced by:  pm4.71 637  biantrud 728  bianfd 740  pm5.71 750  19.33b 1094  sb4b 1226  a16gb 1279  2eu1 1452  2eu3 1454  ceqsalg 1828  undif4 2329  opthpr 2489  elpwuni 2767  iunpw 2920  onint0 3013  ordssun 3085  suc11 3099  unizlim 3119  xp11 3482  imadif 3580  2elresin 3604  f1fveq 3882  oa00 4199  omcan 4206  oecan 4222  nnarcl 4238  nnaordex 4255  nnawordex 4256  erth 4288  fundmen 4434  0sdomg 4472  unidom 4818  cardsdomel 4863  iscard2 4865  cardalephex 4897  cfeq0 4926  axrepnd 4958  cnegextlem1 5357  add20 5614  xrmaxltt 5915  xrltmint 5916  maxlet 5920  lemint 5923  maxltt 5924  xrub 6082  supxrre 6085  iooval2t 6368  uz11t 6433  fzoptht 6503  expeq0t 6586  expcant 6602  sq01t 6652  sqr11 6704  recant 6905  cau3 6916  infdif2 7570  infmap2lem2 7582  istps2 7608  tgval3t 7624  grprcan 8059  grplcan 8071  ip2eqi 8513  hial2eqt 8967  eigorth 9758  stge1 10160  stle0 10161  mdbr3 10219  mdbr4 10220  atsseq 10269  mdsymlem7 10331  oooeqim2 10465  hmeogrp 10524  top1 10533

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