Theorem biimpd 143

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		bi1 117	. 2 |- ( ( ps <-> ch ) -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbid  146  sylibd  148  sylbid  149  mpbidi  150  syl5ib  153  syl6bi  162  ibi  175  imbi1d  230  biimpa  291  notbid  628  mtbird  634  mtbiri  636  orbi2d  740  pm5.15dc  1326  exlimd2  1532  exintr  1571  19.9d  1597  19.23t  1613  dral1  1666  spimt  1672  cbvalh  1684  chvar  1688  exdistrfor  1729  sbequi  1768  spv  1789  eqrdav  2088  cleqh  2188  ceqsalg  2648  vtoclf  2673  vtocl2  2675  vtocl3  2676  spcdv  2705  rspcdv  2726  elabgt  2758  sbcn1  2887  sbcim1  2888  sbcbi1  2889  sbeqalb  2896  sbcel21v  2904  eqrd  3044  exmidsssn  4040  copsexg  4080  euotd  4090  rexxfrd  4298  relop  4599  elres  4761  rnxpid  4878  relcnvtr  4963  iotaval  5004  mpteqb  5406  chfnrn  5424  elpreima  5432  ffnfv  5470  f1elima  5566  f1eqcocnv  5584  fliftfun  5589  isoresbr  5602  isotr  5609  ovmpt2dv2  5792  smoiso  6081  nnaordi  6281  nnaword  6284  nnawordi  6288  xpiderm  6377  iinerm  6378  mptelixpg  6505  dom2lem  6543  nneneq  6627  exmidpw  6678  f1dmvrnfibi  6707  pr2nelem  6880  exmidfodomrlemeldju  6886  exmidfodomrlemreseldju  6887  addcanpig  6954  mulcanpig  6955  enqer  6978  ltexnqi  7029  prarloclemlo  7114  genpcdl  7139  genpcuu  7140  appdivnq  7183  ltprordil  7209  1idprl  7210  1idpru  7211  ltexprlemm  7220  ltexprlemopu  7223  ltexprlemru  7232  cauappcvgprlemladdru  7276  cauappcvgprlemladdrl  7277  caucvgprprlemopu  7319  caucvgsrlemoffcau  7404  caucvgsrlemoffres  7406  ltrenn  7453  axpre-ltadd  7482  addn0nid  7913  apne  8161  prodgt02  8375  prodge02  8377  mulgt1  8385  divgt0  8394  divge0  8395  cju  8482  nnsub  8522  nominpos  8714  zltnle  8857  nn0n0n1ge2  8878  zdcle  8884  btwnnz  8901  uzm1  9110  supinfneg  9144  infsupneg  9145  ublbneg  9159  cnref1o  9194  ltsubrp  9229  ltaddrp  9230  ge0nemnf  9347  xltnegi  9358  iccsupr  9445  icoshft  9468  iccshftri  9473  iccshftli  9475  iccdili  9477  icccntri  9479  fzdcel  9515  fznlem  9516  fzen  9518  fzofzim  9660  eluzgtdifelfzo  9669  elfzonelfzo  9702  qltnle  9718  addmodlteq  9866  fihashf1rn  10258  cjre  10377  caucvgre  10475  icodiamlt  10674  zisum  10835  reeff1  11052  dvds2lem  11147  muldvds1  11160  dvdscmulr  11164  dvdsmulcr  11165  dvdsdivcl  11190  oddnn02np1  11219  ndvdsadd  11270  zeqzmulgcd  11301  bezoutlemmain  11326  dfgcd2  11342  gcdmultiple  11348  coprmdvds  11413  divgcdodd  11461  isprm6  11465  prmdvdsexpr  11468  cncongrprm  11475  phiprmpw  11537  ch2var  11941  bj-rspgt  11959  bj-nntrans  12119  bj-nnelirr  12121  bj-omtrans  12124  setindft  12133  bj-inf2vnlem3  12140  bj-inf2vnlem4  12141  bj-findis  12147