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  3534  pwidg  3620  elpr2  3645  snidg  3652  exsnrex  3665  rabrsndc  3691  prid1g  3727  tpid1g  3735  tpid2g  3737  sssnr  3784  ssprr  3787  sstpr  3788  preqr1  3799  unimax  3874  intmin3  3902  eqbrtrdi  4073  pwnss  4193  0inp0  4200  bnd2  4207  ss1o0el1  4231  exmidsssn  4236  exmidundif  4240  exmidundifim  4241  euabex  4259  copsexg  4278  euotd  4288  elopab  4293  epelg  4326  sucidg  4452  ifelpwung  4517  regexmidlem1  4570  sucprcreg  4586  onprc  4589  dtruex  4596  omelon2  4645  elvvuni  4728  eqrelriv  4757  relopabi  4792  opabid2  4798  ididg  4820  iss  4993  funopg  5293  fn0  5380  f00  5452  f0bi  5453  f1o00  5542  fo00  5543  brprcneu  5554  relelfvdm  5593  fsn  5737  eufnfv  5796  f1eqcocnv  5841  riotaprop  5904  acexmidlemb  5917  acexmidlemab  5919  acexmidlem2  5922  oprabid  5957  elrnmpo  6040  ov6g  6065  eqop2  6245  1stconst  6288  2ndconst  6289  dftpos3  6329  dftpos4  6330  2pwuninelg  6350  frecabcl  6466  el2oss1o  6510  ecopover  6701  map0g  6756  mapsn  6758  elixpsn  6803  en0  6863  en1  6867  fiprc  6883  dom0  6908  nneneq  6927  findcard  6958  findcard2  6959  findcard2s  6960  sbthlem2  7033  sbthlemi4  7035  sbthlemi5  7036  eldju2ndl  7147  updjudhf  7154  enumct  7190  nnnninf  7201  nninfisollem0  7205  fodjuomnilemdc  7219  exmidonfinlem  7272  exmidaclem  7291  pw1ne1  7312  pw1ne3  7313  1ne0sr  7850  00sr  7853  cnm  7916  eqlei2  8138  cnstab  8689  divcanap3  8742  sup3exmid  9001  nn1suc  9026  nn0ge0  9291  xnn0xr  9334  xnn0nemnf  9340  elnn0z  9356  nn0n0n1ge2b  9422  nn0ind-raph  9460  elnn1uz2  9698  indstr2  9700  xrnemnf  9869  xrnepnf  9870  mnfltxr  9878  nn0pnfge0  9883  xrlttr  9887  xrltso  9888  xrlttri3  9889  nltpnft  9906  npnflt  9907  ngtmnft  9909  nmnfgt  9910  xsubge0  9973  xposdif  9974  xleaddadd  9979  fztpval  10175  fseq1p1m1  10186  fz01or  10203  qbtwnxr  10364  xqltnle  10374  fzfig  10539  uzsinds  10553  ser0f  10643  1exp  10677  0exp  10683  bcn1  10867  zfz1iso  10950  0wrd0  10978  wrdlen1  10989  sqrt0rlem  11185  prodf1f  11725  0dvds  11993  nn0o  12089  flodddiv4  12118  bitsp1o  12135  gcddvds  12155  bezoutlemmain  12190  lcmdvds  12272  rpdvds  12292  1nprm  12307  prmind2  12313  nnoddn2prmb  12456  pcpre1  12486  qexpz  12546  4sqlem19  12603  ennnfonelemj0  12643  ennnfonelemhf1o  12655  strslfv  12748  restsspw  12951  xpsfrnel  13046  mgmidcl  13080  mgmlrid  13081  releqgg  13426  islidlm  14111  zrhrhm  14255  psrplusgg  14306  baspartn  14370  eltg3  14377  topnex  14406  discld  14456  lmreltop  14513  cnpfval  14515  cnprcl2k  14526  idcn  14532  xmet0  14683  blfvalps  14705  blfps  14729  blf  14730  limcimolemlt  14984  recnprss  15007  lgsdir2lem2  15354  gausslemma2dlem4  15389  2lgslem2  15417  2lgslem3  15426  2lgs  15429  2sqlem7  15446  funmptd  15533  bj-om  15667  bj-nn0suc0  15680  bj-nn0suc  15694  bj-nn0sucALT  15708  bj-findis  15709  2omap  15726  nninfall  15740  nnnninfen  15752  trilpolemcl  15768  dceqnconst  15791  dcapnconst  15792