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  dedhb  2921  sbceqal  3033  ssdifeq0  3520  pwidg  3604  elpr2  3629  snidg  3636  exsnrex  3649  rabrsndc  3675  prid1g  3711  tpid1g  3719  tpid2g  3721  sssnr  3768  ssprr  3771  sstpr  3772  preqr1  3783  unimax  3858  intmin3  3886  eqbrtrdi  4057  pwnss  4174  0inp0  4181  bnd2  4188  ss1o0el1  4212  exmidsssn  4217  exmidundif  4221  exmidundifim  4222  euabex  4240  copsexg  4259  euotd  4269  elopab  4273  epelg  4305  sucidg  4431  ifelpwung  4496  regexmidlem1  4547  sucprcreg  4563  onprc  4566  dtruex  4573  omelon2  4622  elvvuni  4705  eqrelriv  4734  relopabi  4767  opabid2  4773  ididg  4795  iss  4968  funopg  5265  fn0  5350  f00  5422  f0bi  5423  f1o00  5511  fo00  5512  brprcneu  5523  relelfvdm  5562  fsn  5704  eufnfv  5763  f1eqcocnv  5808  riotaprop  5870  acexmidlemb  5883  acexmidlemab  5885  acexmidlem2  5888  oprabid  5923  elrnmpo  6005  ov6g  6029  eqop2  6197  1stconst  6240  2ndconst  6241  dftpos3  6281  dftpos4  6282  2pwuninelg  6302  frecabcl  6418  el2oss1o  6462  ecopover  6651  map0g  6706  mapsn  6708  elixpsn  6753  en0  6813  en1  6817  fiprc  6833  dom0  6856  nneneq  6875  findcard  6906  findcard2  6907  findcard2s  6908  sbthlem2  6975  sbthlemi4  6977  sbthlemi5  6978  eldju2ndl  7089  updjudhf  7096  enumct  7132  nnnninf  7142  nninfisollem0  7146  fodjuomnilemdc  7160  exmidonfinlem  7210  exmidaclem  7225  pw1ne1  7246  pw1ne3  7247  1ne0sr  7783  00sr  7786  cnm  7849  eqlei2  8070  cnstab  8620  divcanap3  8673  sup3exmid  8932  nn1suc  8956  nn0ge0  9219  xnn0xr  9262  xnn0nemnf  9268  elnn0z  9284  nn0n0n1ge2b  9350  nn0ind-raph  9388  elnn1uz2  9625  indstr2  9627  xrnemnf  9795  xrnepnf  9796  mnfltxr  9804  nn0pnfge0  9809  xrlttr  9813  xrltso  9814  xrlttri3  9815  nltpnft  9832  npnflt  9833  ngtmnft  9835  nmnfgt  9836  xsubge0  9899  xposdif  9900  xleaddadd  9905  fztpval  10101  fseq1p1m1  10112  fz01or  10129  qbtwnxr  10276  fzfig  10448  uzsinds  10460  ser0f  10533  1exp  10567  0exp  10573  bcn1  10756  zfz1iso  10839  sqrt0rlem  11030  prodf1f  11569  0dvds  11836  nn0o  11930  flodddiv4  11957  gcddvds  11982  bezoutlemmain  12017  lcmdvds  12097  rpdvds  12117  1nprm  12132  prmind2  12138  nnoddn2prmb  12280  pcpre1  12310  qexpz  12368  ennnfonelemj0  12420  ennnfonelemhf1o  12432  strslfv  12525  restsspw  12720  xpsfrnel  12786  mgmidcl  12820  mgmlrid  12821  releqgg  13125  islidlm  13756  baspartn  13934  eltg3  13941  topnex  13970  discld  14020  lmreltop  14077  cnpfval  14079  cnprcl2k  14090  idcn  14096  xmet0  14247  blfvalps  14269  blfps  14293  blf  14294  limcimolemlt  14517  recnprss  14540  lgsdir2lem2  14814  2sqlem7  14852  funmptd  14939  bj-om  15073  bj-nn0suc0  15086  bj-nn0suc  15100  bj-nn0sucALT  15114  bj-findis  15115  nninfall  15143  trilpolemcl  15170  dceqnconst  15193  dcapnconst  15194