Theorem biimpd 144

Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		biimp 118	. 2 |- ( ( ps <-> ch ) -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbid  147  sylibd  149  sylbid  150  mpbidi  151  imbitrid  154  syl6bi  163  ibi  176  imbi1d  231  biimpa  296  mtbird  673  mtbiri  675  orbi2d  790  pm5.15dc  1389  exlimd2  1595  exintr  1634  19.9d  1661  19.23t  1677  chvarfv  1700  dral1  1730  spimt  1736  cbvalv1  1751  cbvalh  1753  chvar  1757  exdistrfor  1800  sbequi  1839  spv  1860  cbvexvw  1920  eqrdav  2176  cleqh  2277  ceqsalg  2766  vtoclf  2791  vtocl2  2793  vtocl3  2794  spcdv  2823  rspcdv  2845  elabgt  2879  sbcn1  3011  sbcim1  3012  sbcbi1  3013  sbeqalb  3020  sbcel21v  3028  eqrd  3174  exmidsssn  4203  exmidsssnc  4204  copsexg  4245  euotd  4255  rexxfrd  4464  relop  4778  elres  4944  rnxpid  5064  relcnvtr  5149  iotaval  5190  mpteqb  5607  elfvmptrab  5612  chfnrn  5628  elpreima  5636  ffnfv  5675  f1elima  5774  f1eqcocnv  5792  fliftfun  5797  isoresbr  5810  isotr  5817  ovmpodv2  6008  smoiso  6303  nnaordi  6509  nnaword  6512  nnawordi  6516  xpider  6606  iinerm  6607  mptelixpg  6734  dom2lem  6772  nneneq  6857  exmidpw  6908  f1dmvrnfibi  6943  ismkvnex  7153  pr2nelem  7190  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  netap  7253  2omotaplemap  7256  addcanpig  7333  mulcanpig  7334  enqer  7357  ltexnqi  7408  prarloclemlo  7493  genpcdl  7518  genpcuu  7519  appdivnq  7562  ltprordil  7588  1idprl  7589  1idpru  7590  ltexprlemm  7599  ltexprlemopu  7602  ltexprlemru  7611  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprprlemopu  7698  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  ltrenn  7854  axpre-ltadd  7885  addn0nid  8331  apne  8580  aptap  8607  prodgt02  8810  prodge02  8812  mulgt1  8820  divgt0  8829  divge0  8830  cju  8918  nnsub  8958  nominpos  9156  zltnle  9299  nn0n0n1ge2  9323  zdcle  9329  btwnnz  9347  uzm1  9558  supinfneg  9595  infsupneg  9596  ublbneg  9613  cnref1o  9650  ltsubrp  9690  ltaddrp  9691  xnn0dcle  9802  npnflt  9815  nmnfgt  9818  ge0nemnf  9824  xltnegi  9835  xnn0xadd0  9867  iccsupr  9966  icoshft  9990  iccshftri  9995  iccshftli  9997  iccdili  9999  icccntri  10001  fzdcel  10040  fznlem  10041  fzen  10043  fzofzim  10188  eluzgtdifelfzo  10197  elfzonelfzo  10230  qltnle  10246  addmodlteq  10398  qsqeqor  10631  apexp1  10698  fihashf1rn  10768  cjre  10891  caucvgre  10990  icodiamlt  11189  zsumdc  11392  zproddc  11587  reeff1  11708  dvdsmod0  11800  dvds2lem  11810  muldvds1  11823  dvdscmulr  11827  dvdsmulcr  11828  dvdsdivcl  11856  oddnn02np1  11885  ndvdsadd  11936  zeqzmulgcd  11971  bezoutlemmain  11999  dfgcd2  12015  gcdmultiple  12021  coprmdvds  12092  divgcdodd  12143  isprm6  12147  prmdvdsexpr  12150  cncongrprm  12157  phiprmpw  12222  modprm0  12254  pythagtriplem4  12268  pcz  12331  difsqpwdvds  12337  pcadd  12339  1arith  12365  isgrpid2  12913  ringinvnz1ne0  13226  lmss  13749  cnplimcim  14139  dvcn  14167  lgseisenlem2  14454  2sqlem6  14470  ch2var  14522  bj-rspgt  14541  bj-charfundcALT  14564  bj-nntrans  14706  bj-nnelirr  14708  bj-omtrans  14711  setindft  14720  bj-inf2vnlem3  14727  bj-inf2vnlem4  14728  bj-findis  14734  pw1nct  14755