Theorem biimprd 158

Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimprd.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimprd	|- ( ph -> ( ch -> ps ) )

Proof of Theorem biimprd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2		biimprd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	imbitrrid 156	1 |- ( ph -> ( ch -> ps ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl6bir  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  672  mtbii  674  orbi2d  790  pm4.55dc  938  pm3.11dc  957  prlem1  973  nfimd  1585  dral1  1730  cbvalv1  1751  cbvalh  1753  ax16i  1858  speiv  1862  a16g  1864  cbvalvw  1919  cbvexvw  1920  cleqh  2277  pm13.18  2428  rspcimdv  2843  rspcimedv  2844  rspcedv  2846  moi2  2919  moi  2921  eqrd  3174  abnexg  4447  ralxfrd  4463  ralxfr2d  4465  rexxfr2d  4466  elres  4944  2elresin  5328  f1ocnv  5475  tz6.12c  5546  fvun1  5583  dffo4  5665  isores3  5816  tposfo2  6268  issmo2  6290  iordsmo  6298  smoel2  6304  fiintim  6928  ismkvnex  7153  prarloclemarch  7417  genprndl  7520  genprndu  7521  ltpopr  7594  ltsopr  7595  recexprlem1ssl  7632  recexprlem1ssu  7633  aptiprlemu  7639  lttrsr  7761  aptap  8607  rerecapb  8800  nnmulcl  8940  nnnegz  9256  eluzdc  9610  negm  9615  iccid  9925  icoshft  9990  fzen  10043  elfz2nn0  10112  elfzom1p1elfzo  10214  flqeqceilz  10318  zmodidfzoimp  10354  caucvgre  10990  qdenre  11211  dvdsval2  11797  negdvdsb  11814  muldvds2  11824  dvdsabseq  11853  bezoutlemaz  12004  bezoutlembz  12005  rplpwr  12028  alginv  12047  algfx  12052  coprmgcdb  12088  divgcdcoprm0  12101  prmgt1  12132  oddprmgt2  12134  rpexp1i  12154  2sqpwodd  12176  qnumdencl  12187  phiprmpw  12222  prmdiveq  12236  prm23lt5  12263  pcmpt  12341  infpnlem1  12357  oddennn  12393  nninfdclemf1  12453  imasaddfnlemg  12735  aprcotr  13375  cnpnei  13722  bl2in  13906  addcncntoplem  14054  rescncf  14071  limcresi  14138  cnplimcim  14139  efltlemlt  14198  ioocosf1o  14278  uzdcinzz  14553  bj-charfunbi  14566  bj-omssind  14690  bj-bdfindes  14704  bj-nntrans  14706  bj-nnelirr  14708  bj-omtrans  14711  setindis  14722  bdsetindis  14724  bj-inf2vnlem3  14727  bj-inf2vnlem4  14728  bj-findis  14734  bj-findes  14736