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-mp 5  ax-1 6  ax-2 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  1380  dedhb  2899  sbceqal  3010  ssdifeq0  3497  pwidg  3580  elpr2  3605  snidg  3612  exsnrex  3625  rabrsndc  3651  prid1g  3687  tpid1g  3695  tpid2g  3697  sssnr  3740  ssprr  3743  sstpr  3744  preqr1  3755  unimax  3830  intmin3  3858  eqbrtrdi  4028  pwnss  4145  0inp0  4152  bnd2  4159  ss1o0el1  4183  exmidsssn  4188  exmidundif  4192  exmidundifim  4193  euabex  4210  copsexg  4229  euotd  4239  elopab  4243  epelg  4275  sucidg  4401  ifelpwung  4466  regexmidlem1  4517  sucprcreg  4533  onprc  4536  dtruex  4543  omelon2  4592  elvvuni  4675  eqrelriv  4704  relopabi  4737  opabid2  4742  ididg  4764  iss  4937  funopg  5232  fn0  5317  f00  5389  f0bi  5390  f1o00  5477  fo00  5478  brprcneu  5489  relelfvdm  5528  fsn  5668  eufnfv  5726  f1eqcocnv  5770  riotaprop  5832  acexmidlemb  5845  acexmidlemab  5847  acexmidlem2  5850  oprabid  5885  elrnmpo  5966  ov6g  5990  eqop2  6157  1stconst  6200  2ndconst  6201  dftpos3  6241  dftpos4  6242  2pwuninelg  6262  frecabcl  6378  el2oss1o  6422  ecopover  6611  map0g  6666  mapsn  6668  elixpsn  6713  en0  6773  en1  6777  fiprc  6793  dom0  6816  nneneq  6835  findcard  6866  findcard2  6867  findcard2s  6868  sbthlem2  6935  sbthlemi4  6937  sbthlemi5  6938  eldju2ndl  7049  updjudhf  7056  enumct  7092  nnnninf  7102  nninfisollem0  7106  fodjuomnilemdc  7120  exmidonfinlem  7170  exmidaclem  7185  pw1ne1  7206  pw1ne3  7207  1ne0sr  7728  00sr  7731  cnm  7794  eqlei2  8014  cnstab  8564  divcanap3  8615  sup3exmid  8873  nn1suc  8897  nn0ge0  9160  xnn0xr  9203  xnn0nemnf  9209  elnn0z  9225  nn0n0n1ge2b  9291  nn0ind-raph  9329  elnn1uz2  9566  indstr2  9568  xrnemnf  9734  xrnepnf  9735  mnfltxr  9743  nn0pnfge0  9748  xrlttr  9752  xrltso  9753  xrlttri3  9754  nltpnft  9771  npnflt  9772  ngtmnft  9774  nmnfgt  9775  xsubge0  9838  xposdif  9839  xleaddadd  9844  fztpval  10039  fseq1p1m1  10050  fz01or  10067  qbtwnxr  10214  fzfig  10386  uzsinds  10398  ser0f  10471  1exp  10505  0exp  10511  bcn1  10692  zfz1iso  10776  sqrt0rlem  10967  prodf1f  11506  0dvds  11773  nn0o  11866  flodddiv4  11893  gcddvds  11918  bezoutlemmain  11953  lcmdvds  12033  rpdvds  12053  1nprm  12068  prmind2  12074  nnoddn2prmb  12216  pcpre1  12246  qexpz  12304  ennnfonelemj0  12356  ennnfonelemhf1o  12368  strslfv  12460  restsspw  12589  mgmidcl  12632  mgmlrid  12633  baspartn  12842  eltg3  12851  topnex  12880  discld  12930  lmreltop  12987  cnpfval  12989  cnprcl2k  13000  idcn  13006  xmet0  13157  blfvalps  13179  blfps  13203  blf  13204  limcimolemlt  13427  recnprss  13450  lgsdir2lem2  13724  2sqlem7  13751  funmptd  13838  bj-om  13972  bj-nn0suc0  13985  bj-nn0suc  13999  bj-nn0sucALT  14013  bj-findis  14014  nninfall  14042  trilpolemcl  14069  dceqnconst  14091  dcapnconst  14092