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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.18im  1434  ceqsexv2d  2862  dedhb  2995  sbceqal  3107  ssdifeq0  3610  pwidg  3706  elpr2  3731  snidg  3738  exsnrex  3751  rabrsndc  3779  prid1g  3815  tpid1g  3825  tpid2g  3827  sssnr  3878  ssprr  3881  sstpr  3882  preqr1  3893  unimax  3969  intmin3  3997  eqbrtrdi  4170  if0elpw  4297  pwnss  4298  0inp0  4305  bnd2  4312  ss1o0el1  4336  exmidsssn  4341  exmidundif  4345  exmidundifim  4346  euabex  4367  copsexg  4386  euotd  4397  elopab  4402  epelg  4437  sucidg  4563  ifelpwung  4629  regexmidlem1  4682  sucprcreg  4698  onprc  4701  dtruex  4708  omelon2  4757  elvvuni  4841  eqrelriv  4870  relopabi  4907  opabid2  4913  ididg  4935  iss  5112  funopg  5414  fn0  5506  f00  5587  f0bi  5588  f10d  5678  f1o00  5679  fo00  5680  brprcneu  5691  relelfvdm  5730  fvmbr  5734  fsn  5883  funop  5895  eufnfv  5952  f1eqcocnv  6000  riotaprop  6067  acexmidlemb  6080  acexmidlemab  6082  acexmidlem2  6085  oprabid  6120  elrnmpo  6205  ov6g  6230  eqop2  6416  1stconst  6461  2ndconst  6462  dftpos3  6538  dftpos4  6539  2pwuninelg  6559  frecabcl  6675  el2oss1o  6721  ecopover  6912  map0g  6974  mapsnd  6976  mapsn  6978  elixpsn  7023  en0  7088  en1  7092  fiprc  7110  en2m  7119  dom0  7144  nneneq  7164  findcard  7198  findcard2  7199  findcard2s  7200  elssdc  7215  eqsndc  7216  sbthlem2  7282  sbthlemi4  7284  sbthlemi5  7285  2omap  7325  eldju2ndl  7419  updjudhf  7426  enumct  7462  nnnninf  7473  nninfisollem0  7477  fodjuomnilemdc  7491  exmidonfinlem  7552  exmidaclem  7571  pw1ne1  7595  pw1ne3  7596  1ne0sr  8140  00sr  8143  cnm  8206  eqlei2  8428  cnstab  8982  divcanap3  9037  sup3exmid  9296  nn1suc  9333  nn0ge0  9600  xnn0xr  9645  xnn0nemnf  9651  elnn0z  9667  nn0n0n1ge2b  9735  nn0ind-raph  9774  elnn1uz2  10023  indstr2  10025  xrnemnf  10196  xrnepnf  10197  mnfltxr  10205  nn0pnfge0  10210  xrlttr  10214  xrltso  10215  xrlttri3  10216  nltpnft  10233  npnflt  10234  ngtmnft  10236  nmnfgt  10237  xsubge0  10300  xposdif  10301  xleaddadd  10306  fztpval  10507  fseq1p1m1  10518  fz01or  10535  qbtwnxr  10709  xqltnle  10719  fzfig  10888  uzsinds  10902  ser0f  10992  1exp  11026  0exp  11032  bcn1  11218  en1hash  11261  hashfibc  11305  hashf1  11309  zfz1iso  11315  hash2en  11317  0wrd0  11352  wrdlen1  11364  wrdl1exs1  11419  swrdspsleq  11461  cats1un  11515  wrdind  11516  wrd2ind  11517  sq01  11682  sqrt0rlem  11791  fzf1o  12167  prodf1f  12335  0dvds  12603  nn0o  12699  flodddiv4  12728  bitsp1o  12745  gcddvds  12765  bezoutlemmain  12800  lcmdvds  12882  rpdvds  12902  1nprm  12917  prmind2  12923  nnoddn2prmb  13070  pcpre1  13100  qexpz  13160  4sqlem19  13217  prmlem0  13249  ballotfilem8  13338  ennnfonelemj0  13350  ennnfonelemhf1o  13362  strslfv  13455  restsspw  13662  xpsfrnel  13724  mgmidcl  13757  mgmlrid  13758  releqgg  14082  cntzrcl  14159  gzsumgsum1  14243  gsumcom2fi  14275  islidlm  14925  zrhrhm  15067  psrplusgg  15201  psrridmfi  15220  mplsubrgfi  15250  baspartn  15309  eltg3  15316  topnex  15345  discld  15395  cnpfval  15454  cnprcl2k  15465  idcn  15471  xmet0  15622  blfvalps  15644  blfps  15668  blf  15669  limcimolemlt  15923  recnprss  15946  bposlem6  16349  lgsdir2lem2  16386  gausslemma2dlem4  16421  2lgslem2  16449  2lgslem3  16458  2lgs  16461  2sqlem7  16478  uhgr0e  16561  incistruhgr  16569  issubgr2  16737  subgrprop2  16739  egrsubgr  16742  0grsubgr  16743  0uhgrsubgr  16744  uhgrsubgrself  16745  clwwlkn1  16897  funmptd  17069  bj-om  17201  bj-nn0suc0  17214  bj-nn0suc  17228  bj-nn0sucALT  17242  bj-findis  17243  pw1map  17263  wexmiddiffilem  17281  wexmiddifxylem  17283  nninfall  17291  nnnninfen  17303  trilpolemcl  17326  dceqnconst  17350  dcapnconst  17351