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  2853  dedhb  2985  sbceqal  3097  ssdifeq0  3591  pwidg  3685  elpr2  3710  snidg  3717  exsnrex  3730  rabrsndc  3758  prid1g  3794  tpid1g  3803  tpid2g  3805  sssnr  3856  ssprr  3859  sstpr  3860  preqr1  3871  unimax  3947  intmin3  3975  eqbrtrdi  4147  if0elpw  4270  pwnss  4271  0inp0  4278  bnd2  4285  ss1o0el1  4309  exmidsssn  4314  exmidundif  4318  exmidundifim  4319  euabex  4340  copsexg  4359  euotd  4370  elopab  4375  epelg  4410  sucidg  4536  ifelpwung  4601  regexmidlem1  4654  sucprcreg  4670  onprc  4673  dtruex  4680  omelon2  4729  elvvuni  4813  eqrelriv  4842  relopabi  4879  opabid2  4885  ididg  4907  iss  5083  funopg  5385  fn0  5477  f00  5558  f0bi  5559  f10d  5649  f1o00  5650  fo00  5651  brprcneu  5662  relelfvdm  5701  fvmbr  5704  fsn  5848  funop  5860  eufnfv  5916  f1eqcocnv  5963  riotaprop  6028  acexmidlemb  6041  acexmidlemab  6043  acexmidlem2  6046  oprabid  6081  elrnmpo  6166  ov6g  6191  eqop2  6371  1stconst  6416  2ndconst  6417  dftpos3  6492  dftpos4  6493  2pwuninelg  6513  frecabcl  6629  el2oss1o  6675  ecopover  6866  map0g  6921  mapsnd  6922  mapsn  6924  elixpsn  6969  en0  7034  en1  7038  fiprc  7056  en2m  7065  dom0  7090  nneneq  7110  findcard  7144  findcard2  7145  findcard2s  7146  elssdc  7161  eqsndc  7162  sbthlem2  7227  sbthlemi4  7229  sbthlemi5  7230  2omap  7268  eldju2ndl  7362  updjudhf  7369  enumct  7405  nnnninf  7416  nninfisollem0  7420  fodjuomnilemdc  7434  exmidonfinlem  7495  exmidaclem  7514  pw1ne1  7538  pw1ne3  7539  1ne0sr  8080  00sr  8083  cnm  8146  eqlei2  8367  cnstab  8918  divcanap3  8971  sup3exmid  9230  nn1suc  9255  nn0ge0  9520  xnn0xr  9567  xnn0nemnf  9573  elnn0z  9589  nn0n0n1ge2b  9656  nn0ind-raph  9694  elnn1uz2  9938  indstr2  9940  xrnemnf  10109  xrnepnf  10110  mnfltxr  10118  nn0pnfge0  10123  xrlttr  10127  xrltso  10128  xrlttri3  10129  nltpnft  10146  npnflt  10147  ngtmnft  10149  nmnfgt  10150  xsubge0  10213  xposdif  10214  xleaddadd  10219  fztpval  10416  fseq1p1m1  10427  fz01or  10444  qbtwnxr  10616  xqltnle  10626  fzfig  10791  uzsinds  10805  ser0f  10895  1exp  10929  0exp  10935  bcn1  11119  en1hash  11161  hashfibc  11203  zfz1iso  11209  hash2en  11211  0wrd0  11246  wrdlen1  11258  wrdl1exs1  11313  swrdspsleq  11355  cats1un  11409  wrdind  11410  wrd2ind  11411  sqrt0rlem  11684  fzf1o  12057  prodf1f  12225  0dvds  12493  nn0o  12589  flodddiv4  12618  bitsp1o  12635  gcddvds  12655  bezoutlemmain  12690  lcmdvds  12772  rpdvds  12792  1nprm  12807  prmind2  12813  nnoddn2prmb  12956  pcpre1  12986  qexpz  13046  4sqlem19  13103  ennnfonelemj0  13144  ennnfonelemhf1o  13156  strslfv  13249  restsspw  13454  xpsfrnel  13549  mgmidcl  13583  mgmlrid  13584  releqgg  13929  islidlm  14619  zrhrhm  14763  psrplusgg  14825  baspartn  14907  eltg3  14914  topnex  14943  discld  14993  cnpfval  15052  cnprcl2k  15063  idcn  15069  xmet0  15220  blfvalps  15242  blfps  15266  blf  15267  limcimolemlt  15521  recnprss  15544  lgsdir2lem2  15894  gausslemma2dlem4  15929  2lgslem2  15957  2lgslem3  15966  2lgs  15969  2sqlem7  15986  uhgr0e  16069  incistruhgr  16077  issubgr2  16245  subgrprop2  16247  egrsubgr  16250  0grsubgr  16251  0uhgrsubgr  16252  uhgrsubgrself  16253  clwwlkn1  16405  funmptd  16567  bj-om  16699  bj-nn0suc0  16712  bj-nn0suc  16726  bj-nn0sucALT  16740  bj-findis  16741  pw1map  16761  nninfall  16779  nnnninfen  16791  trilpolemcl  16813  dceqnconst  16837  dcapnconst  16838  gsumgfsum1  16854