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  1385  dedhb  2906  sbceqal  3018  ssdifeq0  3505  pwidg  3588  elpr2  3613  snidg  3620  exsnrex  3633  rabrsndc  3659  prid1g  3695  tpid1g  3703  tpid2g  3705  sssnr  3751  ssprr  3754  sstpr  3755  preqr1  3766  unimax  3841  intmin3  3869  eqbrtrdi  4039  pwnss  4156  0inp0  4163  bnd2  4170  ss1o0el1  4194  exmidsssn  4199  exmidundif  4203  exmidundifim  4204  euabex  4222  copsexg  4241  euotd  4251  elopab  4255  epelg  4287  sucidg  4413  ifelpwung  4478  regexmidlem1  4529  sucprcreg  4545  onprc  4548  dtruex  4555  omelon2  4604  elvvuni  4687  eqrelriv  4716  relopabi  4749  opabid2  4754  ididg  4776  iss  4949  funopg  5246  fn0  5331  f00  5403  f0bi  5404  f1o00  5492  fo00  5493  brprcneu  5504  relelfvdm  5543  fsn  5684  eufnfv  5742  f1eqcocnv  5786  riotaprop  5848  acexmidlemb  5861  acexmidlemab  5863  acexmidlem2  5866  oprabid  5901  elrnmpo  5982  ov6g  6006  eqop2  6173  1stconst  6216  2ndconst  6217  dftpos3  6257  dftpos4  6258  2pwuninelg  6278  frecabcl  6394  el2oss1o  6438  ecopover  6627  map0g  6682  mapsn  6684  elixpsn  6729  en0  6789  en1  6793  fiprc  6809  dom0  6832  nneneq  6851  findcard  6882  findcard2  6883  findcard2s  6884  sbthlem2  6951  sbthlemi4  6953  sbthlemi5  6954  eldju2ndl  7065  updjudhf  7072  enumct  7108  nnnninf  7118  nninfisollem0  7122  fodjuomnilemdc  7136  exmidonfinlem  7186  exmidaclem  7201  pw1ne1  7222  pw1ne3  7223  1ne0sr  7756  00sr  7759  cnm  7822  eqlei2  8042  cnstab  8592  divcanap3  8644  sup3exmid  8903  nn1suc  8927  nn0ge0  9190  xnn0xr  9233  xnn0nemnf  9239  elnn0z  9255  nn0n0n1ge2b  9321  nn0ind-raph  9359  elnn1uz2  9596  indstr2  9598  xrnemnf  9764  xrnepnf  9765  mnfltxr  9773  nn0pnfge0  9778  xrlttr  9782  xrltso  9783  xrlttri3  9784  nltpnft  9801  npnflt  9802  ngtmnft  9804  nmnfgt  9805  xsubge0  9868  xposdif  9869  xleaddadd  9874  fztpval  10069  fseq1p1m1  10080  fz01or  10097  qbtwnxr  10244  fzfig  10416  uzsinds  10428  ser0f  10501  1exp  10535  0exp  10541  bcn1  10722  zfz1iso  10805  sqrt0rlem  10996  prodf1f  11535  0dvds  11802  nn0o  11895  flodddiv4  11922  gcddvds  11947  bezoutlemmain  11982  lcmdvds  12062  rpdvds  12082  1nprm  12097  prmind2  12103  nnoddn2prmb  12245  pcpre1  12275  qexpz  12333  ennnfonelemj0  12385  ennnfonelemhf1o  12397  strslfv  12489  restsspw  12646  mgmidcl  12689  mgmlrid  12690  baspartn  13215  eltg3  13224  topnex  13253  discld  13303  lmreltop  13360  cnpfval  13362  cnprcl2k  13373  idcn  13379  xmet0  13530  blfvalps  13552  blfps  13576  blf  13577  limcimolemlt  13800  recnprss  13823  lgsdir2lem2  14097  2sqlem7  14124  funmptd  14211  bj-om  14345  bj-nn0suc0  14358  bj-nn0suc  14372  bj-nn0sucALT  14386  bj-findis  14387  nninfall  14414  trilpolemcl  14441  dceqnconst  14463  dcapnconst  14464