Theorem mpbiri 168

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 167	1 |- ( ph -> 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:  pm5.18im  1430  ceqsexv2d  2844  dedhb  2976  sbceqal  3088  ssdifeq0  3579  pwidg  3670  elpr2  3695  snidg  3702  exsnrex  3715  rabrsndc  3743  prid1g  3779  tpid1g  3788  tpid2g  3790  sssnr  3841  ssprr  3844  sstpr  3845  preqr1  3856  unimax  3932  intmin3  3960  eqbrtrdi  4132  if0elpw  4254  pwnss  4255  0inp0  4262  bnd2  4269  ss1o0el1  4293  exmidsssn  4298  exmidundif  4302  exmidundifim  4303  euabex  4323  copsexg  4342  euotd  4353  elopab  4358  epelg  4393  sucidg  4519  ifelpwung  4584  regexmidlem1  4637  sucprcreg  4653  onprc  4656  dtruex  4663  omelon2  4712  elvvuni  4796  eqrelriv  4825  relopabi  4861  opabid2  4867  ididg  4889  iss  5065  funopg  5367  fn0  5459  f00  5537  f0bi  5538  f10d  5628  f1o00  5629  fo00  5630  brprcneu  5641  relelfvdm  5680  fvmbr  5683  fsn  5827  funop  5839  eufnfv  5895  f1eqcocnv  5942  riotaprop  6007  acexmidlemb  6020  acexmidlemab  6022  acexmidlem2  6025  oprabid  6060  elrnmpo  6145  ov6g  6170  eqop2  6350  1stconst  6395  2ndconst  6396  dftpos3  6471  dftpos4  6472  2pwuninelg  6492  frecabcl  6608  el2oss1o  6654  ecopover  6845  map0g  6900  mapsn  6902  elixpsn  6947  en0  7012  en1  7016  fiprc  7033  en2m  7042  dom0  7067  nneneq  7086  findcard  7120  findcard2  7121  findcard2s  7122  elssdc  7137  eqsndc  7138  sbthlem2  7200  sbthlemi4  7202  sbthlemi5  7203  eldju2ndl  7314  updjudhf  7321  enumct  7357  nnnninf  7368  nninfisollem0  7372  fodjuomnilemdc  7386  exmidonfinlem  7447  exmidaclem  7466  pw1ne1  7490  pw1ne3  7491  1ne0sr  8029  00sr  8032  cnm  8095  eqlei2  8317  cnstab  8868  divcanap3  8921  sup3exmid  9180  nn1suc  9205  nn0ge0  9470  xnn0xr  9513  xnn0nemnf  9519  elnn0z  9535  nn0n0n1ge2b  9602  nn0ind-raph  9640  elnn1uz2  9884  indstr2  9886  xrnemnf  10055  xrnepnf  10056  mnfltxr  10064  nn0pnfge0  10069  xrlttr  10073  xrltso  10074  xrlttri3  10075  nltpnft  10092  npnflt  10093  ngtmnft  10095  nmnfgt  10096  xsubge0  10159  xposdif  10160  xleaddadd  10165  fztpval  10361  fseq1p1m1  10372  fz01or  10389  qbtwnxr  10561  xqltnle  10571  fzfig  10736  uzsinds  10750  ser0f  10840  1exp  10874  0exp  10880  bcn1  11064  en1hash  11106  zfz1iso  11149  hash2en  11151  0wrd0  11186  wrdlen1  11198  wrdl1exs1  11253  swrdspsleq  11295  cats1un  11349  wrdind  11350  wrd2ind  11351  sqrt0rlem  11624  fzf1o  11997  prodf1f  12165  0dvds  12433  nn0o  12529  flodddiv4  12558  bitsp1o  12575  gcddvds  12595  bezoutlemmain  12630  lcmdvds  12712  rpdvds  12732  1nprm  12747  prmind2  12753  nnoddn2prmb  12896  pcpre1  12926  qexpz  12986  4sqlem19  13043  ennnfonelemj0  13083  ennnfonelemhf1o  13095  strslfv  13188  restsspw  13393  xpsfrnel  13488  mgmidcl  13522  mgmlrid  13523  releqgg  13868  islidlm  14555  zrhrhm  14699  psrplusgg  14759  baspartn  14841  eltg3  14848  topnex  14877  discld  14927  cnpfval  14986  cnprcl2k  14997  idcn  15003  xmet0  15154  blfvalps  15176  blfps  15200  blf  15201  limcimolemlt  15455  recnprss  15478  lgsdir2lem2  15828  gausslemma2dlem4  15863  2lgslem2  15891  2lgslem3  15900  2lgs  15903  2sqlem7  15920  uhgr0e  16003  incistruhgr  16011  issubgr2  16179  subgrprop2  16181  egrsubgr  16184  0grsubgr  16185  0uhgrsubgr  16186  uhgrsubgrself  16187  clwwlkn1  16339  funmptd  16501  bj-om  16633  bj-nn0suc0  16646  bj-nn0suc  16660  bj-nn0sucALT  16674  bj-findis  16675  2omap  16695  pw1map  16697  nninfall  16715  nnnninfen  16727  trilpolemcl  16749  dceqnconst  16773  dcapnconst  16774  gsumgfsum1  16790