Theorem mpbiri 167

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mpbiri.min	|- ch
mpbiri.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mpbiri	|- ( ph -> ps )

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 |- ch
2	1	a1i 9	. 2 |- ( ph -> ch )
3		mpbiri.maj	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	mpbird 166	1 |- ( ph -> ps )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.18im  1364  dedhb  2857  sbceqal  2968  ssdifeq0  3450  pwidg  3529  elpr2  3554  snidg  3561  exsnrex  3573  rabrsndc  3599  prid1g  3635  tpid1g  3643  tpid2g  3645  sssnr  3688  ssprr  3691  sstpr  3692  preqr1  3703  unimax  3778  intmin3  3806  eqbrtrdi  3975  pwnss  4091  0inp0  4098  bnd2  4105  exmid01  4129  exmidsssn  4133  exmidundif  4137  exmidundifim  4138  euabex  4155  copsexg  4174  euotd  4184  elopab  4188  epelg  4220  sucidg  4346  regexmidlem1  4456  sucprcreg  4472  onprc  4475  dtruex  4482  omelon2  4529  elvvuni  4611  eqrelriv  4640  relopabi  4673  opabid2  4678  ididg  4700  iss  4873  funopg  5165  fn0  5250  f00  5322  f0bi  5323  f1o00  5410  fo00  5411  brprcneu  5422  relelfvdm  5461  fsn  5600  eufnfv  5656  f1eqcocnv  5700  riotaprop  5761  acexmidlemb  5774  acexmidlemab  5776  acexmidlem2  5779  oprabid  5811  elrnmpo  5892  ov6g  5916  eqop2  6084  1stconst  6126  2ndconst  6127  dftpos3  6167  dftpos4  6168  2pwuninelg  6188  frecabcl  6304  ecopover  6535  map0g  6590  mapsn  6592  elixpsn  6637  en0  6697  en1  6701  fiprc  6717  dom0  6740  nneneq  6759  findcard  6790  findcard2  6791  findcard2s  6792  sbthlem2  6854  sbthlemi4  6856  sbthlemi5  6857  eldju2ndl  6965  updjudhf  6972  enumct  7008  fodjuomnilemdc  7024  nnnninf  7031  exmidonfinlem  7066  exmidaclem  7081  1ne0sr  7598  00sr  7601  cnm  7664  eqlei2  7882  divcanap3  8482  sup3exmid  8739  nn1suc  8763  nn0ge0  9026  xnn0xr  9069  xnn0nemnf  9075  elnn0z  9091  nn0n0n1ge2b  9154  nn0ind-raph  9192  elnn1uz2  9428  indstr2  9430  xrnemnf  9594  xrnepnf  9595  mnfltxr  9602  nn0pnfge0  9607  xrlttr  9611  xrltso  9612  xrlttri3  9613  nltpnft  9627  npnflt  9628  ngtmnft  9630  nmnfgt  9631  xsubge0  9694  xposdif  9695  xleaddadd  9700  fztpval  9894  fseq1p1m1  9905  fz01or  9922  qbtwnxr  10066  fzfig  10234  uzsinds  10246  ser0f  10319  1exp  10353  0exp  10359  bcn1  10536  zfz1iso  10616  sqrt0rlem  10807  prodf1f  11344  0dvds  11549  nn0o  11640  flodddiv4  11667  gcddvds  11688  bezoutlemmain  11722  lcmdvds  11796  rpdvds  11816  1nprm  11831  prmind2  11837  ennnfonelemj0  11950  ennnfonelemhf1o  11962  strslfv  12042  restsspw  12169  baspartn  12256  eltg3  12265  topnex  12294  discld  12344  lmreltop  12401  cnpfval  12403  cnprcl2k  12414  idcn  12420  xmet0  12571  blfvalps  12593  blfps  12617  blf  12618  limcimolemlt  12841  recnprss  12864  bj-om  13306  bj-nn0suc0  13319  bj-nn0suc  13333  bj-nn0sucALT  13347  bj-findis  13348  el2oss1o  13359  nninfall  13379  trilpolemcl  13405  dceqnconst  13423