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  1385  dedhb  2907  sbceqal  3019  ssdifeq0  3506  pwidg  3590  elpr2  3615  snidg  3622  exsnrex  3635  rabrsndc  3661  prid1g  3697  tpid1g  3705  tpid2g  3707  sssnr  3754  ssprr  3757  sstpr  3758  preqr1  3769  unimax  3844  intmin3  3872  eqbrtrdi  4043  pwnss  4160  0inp0  4167  bnd2  4174  ss1o0el1  4198  exmidsssn  4203  exmidundif  4207  exmidundifim  4208  euabex  4226  copsexg  4245  euotd  4255  elopab  4259  epelg  4291  sucidg  4417  ifelpwung  4482  regexmidlem1  4533  sucprcreg  4549  onprc  4552  dtruex  4559  omelon2  4608  elvvuni  4691  eqrelriv  4720  relopabi  4753  opabid2  4759  ididg  4781  iss  4954  funopg  5251  fn0  5336  f00  5408  f0bi  5409  f1o00  5497  fo00  5498  brprcneu  5509  relelfvdm  5548  fsn  5689  eufnfv  5748  f1eqcocnv  5792  riotaprop  5854  acexmidlemb  5867  acexmidlemab  5869  acexmidlem2  5872  oprabid  5907  elrnmpo  5988  ov6g  6012  eqop2  6179  1stconst  6222  2ndconst  6223  dftpos3  6263  dftpos4  6264  2pwuninelg  6284  frecabcl  6400  el2oss1o  6444  ecopover  6633  map0g  6688  mapsn  6690  elixpsn  6735  en0  6795  en1  6799  fiprc  6815  dom0  6838  nneneq  6857  findcard  6888  findcard2  6889  findcard2s  6890  sbthlem2  6957  sbthlemi4  6959  sbthlemi5  6960  eldju2ndl  7071  updjudhf  7078  enumct  7114  nnnninf  7124  nninfisollem0  7128  fodjuomnilemdc  7142  exmidonfinlem  7192  exmidaclem  7207  pw1ne1  7228  pw1ne3  7229  1ne0sr  7765  00sr  7768  cnm  7831  eqlei2  8052  cnstab  8602  divcanap3  8655  sup3exmid  8914  nn1suc  8938  nn0ge0  9201  xnn0xr  9244  xnn0nemnf  9250  elnn0z  9266  nn0n0n1ge2b  9332  nn0ind-raph  9370  elnn1uz2  9607  indstr2  9609  xrnemnf  9777  xrnepnf  9778  mnfltxr  9786  nn0pnfge0  9791  xrlttr  9795  xrltso  9796  xrlttri3  9797  nltpnft  9814  npnflt  9815  ngtmnft  9817  nmnfgt  9818  xsubge0  9881  xposdif  9882  xleaddadd  9887  fztpval  10083  fseq1p1m1  10094  fz01or  10111  qbtwnxr  10258  fzfig  10430  uzsinds  10442  ser0f  10515  1exp  10549  0exp  10555  bcn1  10738  zfz1iso  10821  sqrt0rlem  11012  prodf1f  11551  0dvds  11818  nn0o  11912  flodddiv4  11939  gcddvds  11964  bezoutlemmain  11999  lcmdvds  12079  rpdvds  12099  1nprm  12114  prmind2  12120  nnoddn2prmb  12262  pcpre1  12292  qexpz  12350  ennnfonelemj0  12402  ennnfonelemhf1o  12414  strslfv  12507  restsspw  12698  xpsfrnel  12763  mgmidcl  12797  mgmlrid  12798  releqgg  13080  baspartn  13553  eltg3  13560  topnex  13589  discld  13639  lmreltop  13696  cnpfval  13698  cnprcl2k  13709  idcn  13715  xmet0  13866  blfvalps  13888  blfps  13912  blf  13913  limcimolemlt  14136  recnprss  14159  lgsdir2lem2  14433  2sqlem7  14471  funmptd  14558  bj-om  14692  bj-nn0suc0  14705  bj-nn0suc  14719  bj-nn0sucALT  14733  bj-findis  14734  nninfall  14761  trilpolemcl  14788  dceqnconst  14810  dcapnconst  14811