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-1 5  ax-2 6  ax-mp 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  1322  dedhb  2787  sbceqal  2897  ssdifeq0  3371  pwidg  3449  elpr2  3474  snidg  3479  exsnrex  3491  rabrsndc  3516  prid1g  3552  tpid1g  3560  tpid2g  3562  sssnr  3605  ssprr  3608  sstpr  3609  preqr1  3620  unimax  3695  intmin3  3723  syl6eqbr  3890  pwnss  4002  0inp0  4009  bnd2  4016  exmid01  4040  exmidsssn  4042  exmidundif  4045  exmidundifim  4046  euabex  4063  copsexg  4082  euotd  4092  elopab  4096  epelg  4128  sucidg  4254  regexmidlem1  4364  sucprcreg  4380  onprc  4383  dtruex  4390  omelon2  4437  elvvuni  4517  eqrelriv  4546  relopabi  4578  opabid2  4582  ididg  4604  iss  4773  funopg  5063  fn0  5148  f00  5217  f0bi  5218  f1o00  5303  fo00  5304  brprcneu  5313  relelfvdm  5351  fsn  5485  eufnfv  5541  f1eqcocnv  5586  riotaprop  5647  acexmidlemb  5660  acexmidlemab  5662  acexmidlem2  5665  oprabid  5697  elrnmpt2  5774  ov6g  5798  eqop2  5964  1stconst  6002  2ndconst  6003  dftpos3  6043  dftpos4  6044  2pwuninelg  6064  frecabcl  6180  ecopover  6406  map0g  6461  mapsn  6463  elixpsn  6508  en0  6568  en1  6572  fiprc  6588  dom0  6610  nneneq  6629  findcard  6660  findcard2  6661  findcard2s  6662  sbthlem2  6723  sbthlemi4  6725  sbthlemi5  6726  eldju2ndl  6819  updjudhf  6826  enumct  6849  fodjuomnilemdc  6862  nnnninf  6869  1ne0sr  7375  00sr  7378  eqlei2  7642  divcanap3  8228  nn1suc  8504  nn0ge0  8761  xnn0xr  8804  xnn0nemnf  8810  elnn0z  8826  nn0n0n1ge2b  8889  nn0ind-raph  8926  elnn1uz2  9157  indstr2  9159  xrnemnf  9311  xrnepnf  9312  mnfltxr  9319  nn0pnfge0  9324  xrlttr  9328  xrltso  9329  xrlttri3  9330  nltpnft  9342  ngtmnft  9343  fztpval  9560  fseq1p1m1  9571  fz01or  9588  qbtwnxr  9732  fzfig  9900  uzsinds  9911  iser0f  10011  ser0f  10013  1exp  10047  0exp  10053  bcn1  10229  zfz1iso  10309  sqrt0rlem  10499  0dvds  11157  nn0o  11248  flodddiv4  11275  gcddvds  11296  bezoutlemmain  11328  lcmdvds  11402  rpdvds  11422  1nprm  11437  prmind2  11443  strslfv  11601  restsspw  11725  baspartn  11811  eltg3  11820  topnex  11849  discld  11899  bj-om  12136  bj-nn0suc0  12149  bj-nn0suc  12163  bj-nn0sucALT  12177  bj-findis  12178  el2oss1o  12191  nninfall  12203