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  1396  ceqsexv2d  2803  dedhb  2933  sbceqal  3045  ssdifeq0  3533  pwidg  3619  elpr2  3644  snidg  3651  exsnrex  3664  rabrsndc  3690  prid1g  3726  tpid1g  3734  tpid2g  3736  sssnr  3783  ssprr  3786  sstpr  3787  preqr1  3798  unimax  3873  intmin3  3901  eqbrtrdi  4072  pwnss  4192  0inp0  4199  bnd2  4206  ss1o0el1  4230  exmidsssn  4235  exmidundif  4239  exmidundifim  4240  euabex  4258  copsexg  4277  euotd  4287  elopab  4292  epelg  4325  sucidg  4451  ifelpwung  4516  regexmidlem1  4569  sucprcreg  4585  onprc  4588  dtruex  4595  omelon2  4644  elvvuni  4727  eqrelriv  4756  relopabi  4791  opabid2  4797  ididg  4819  iss  4992  funopg  5292  fn0  5377  f00  5449  f0bi  5450  f1o00  5539  fo00  5540  brprcneu  5551  relelfvdm  5590  fsn  5734  eufnfv  5793  f1eqcocnv  5838  riotaprop  5901  acexmidlemb  5914  acexmidlemab  5916  acexmidlem2  5919  oprabid  5954  elrnmpo  6036  ov6g  6061  eqop2  6236  1stconst  6279  2ndconst  6280  dftpos3  6320  dftpos4  6321  2pwuninelg  6341  frecabcl  6457  el2oss1o  6501  ecopover  6692  map0g  6747  mapsn  6749  elixpsn  6794  en0  6854  en1  6858  fiprc  6874  dom0  6899  nneneq  6918  findcard  6949  findcard2  6950  findcard2s  6951  sbthlem2  7024  sbthlemi4  7026  sbthlemi5  7027  eldju2ndl  7138  updjudhf  7145  enumct  7181  nnnninf  7192  nninfisollem0  7196  fodjuomnilemdc  7210  exmidonfinlem  7260  exmidaclem  7275  pw1ne1  7296  pw1ne3  7297  1ne0sr  7833  00sr  7836  cnm  7899  eqlei2  8121  cnstab  8672  divcanap3  8725  sup3exmid  8984  nn1suc  9009  nn0ge0  9274  xnn0xr  9317  xnn0nemnf  9323  elnn0z  9339  nn0n0n1ge2b  9405  nn0ind-raph  9443  elnn1uz2  9681  indstr2  9683  xrnemnf  9852  xrnepnf  9853  mnfltxr  9861  nn0pnfge0  9866  xrlttr  9870  xrltso  9871  xrlttri3  9872  nltpnft  9889  npnflt  9890  ngtmnft  9892  nmnfgt  9893  xsubge0  9956  xposdif  9957  xleaddadd  9962  fztpval  10158  fseq1p1m1  10169  fz01or  10186  qbtwnxr  10347  xqltnle  10357  fzfig  10522  uzsinds  10536  ser0f  10626  1exp  10660  0exp  10666  bcn1  10850  zfz1iso  10933  0wrd0  10961  wrdlen1  10972  sqrt0rlem  11168  prodf1f  11708  0dvds  11976  nn0o  12072  flodddiv4  12101  bitsp1o  12117  gcddvds  12130  bezoutlemmain  12165  lcmdvds  12247  rpdvds  12267  1nprm  12282  prmind2  12288  nnoddn2prmb  12431  pcpre1  12461  qexpz  12521  4sqlem19  12578  ennnfonelemj0  12618  ennnfonelemhf1o  12630  strslfv  12723  restsspw  12920  xpsfrnel  12987  mgmidcl  13021  mgmlrid  13022  releqgg  13350  islidlm  14035  zrhrhm  14179  psrplusgg  14230  baspartn  14286  eltg3  14293  topnex  14322  discld  14372  lmreltop  14429  cnpfval  14431  cnprcl2k  14442  idcn  14448  xmet0  14599  blfvalps  14621  blfps  14645  blf  14646  limcimolemlt  14900  recnprss  14923  lgsdir2lem2  15270  gausslemma2dlem4  15305  2lgslem2  15333  2lgslem3  15342  2lgs  15345  2sqlem7  15362  funmptd  15449  bj-om  15583  bj-nn0suc0  15596  bj-nn0suc  15610  bj-nn0sucALT  15624  bj-findis  15625  nninfall  15653  nnnninfen  15665  trilpolemcl  15681  dceqnconst  15704  dcapnconst  15705