Theorem mpbiri 224

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 10	. 2 |- (ph -> ch)
3		mpbiri.maj	. 2 |- (ph -> (ps <-> ch))
4	2, 3	mpbird 223	1 |- (ph -> ps)

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  dedt  923  nfald2  1972  nfabd2  2508  dedhb  3007  sbceqal  3098  ssdifeq0  3633  r19.2zb  3641  dedth  3704  pwidg  3735  elpr2  3753  snidg  3759  ifpr  3775  prid1g  3826  pwpw0  3856  sssn  3865  pwsnALT  3883  unimax  3926  intmin3  3955  preqr1  4125  el1c  4140  eqpw1  4163  elxpk  4197  opkabssvvk  4209  cokrelk  4285  abexv  4325  eqpw1uni  4331  pw1equn  4332  pw1eqadj  4333  sspw12  4337  iotassuni  4356  0cnsuc  4402  nnc0suc  4413  nnsucelr  4429  nndisjeq  4430  snfi  4432  lefinrflx  4468  lenltfin  4470  ncfinprop  4475  ncfinraise  4482  ncfinlower  4484  tfinltfinlem1  4501  evenodddisj  4517  sfintfin  4533  sfinltfin  4536  vfinspsslem1  4551  vfinspss  4552  proj1op  4601  copsexg  4608  syl6eqbr  4677  elopab  4697  brsi  4762  br1st  4859  br2nd  4860  brswap2  4861  ididg  4872  iss  5001  dmxpss  5053  xpexr  5110  fn0  5203  f00  5250  f1o00  5318  fo00  5319  dffn5  5364  fvopab4t  5386  fsn  5433  fvi  5443  fconstfv  5457  brswap  5510  oprabid  5551  ov6g  5601  ovelrn  5609  caovmo  5646  op1st2nd  5791  txpcofun  5804  mapsspm  6022  mapsspw  6023  map0e  6024  map0  6026  mapsn  6027  en0  6043  xpassen  6058  enprmaplem5  6081  nenpw1pwlem2  6086  elncs  6120  ncseqnc  6129  eqnc2  6130  1cnc  6140  ncdisjeq  6149  peano4nc  6151  2p1e3c  6157  eqtc  6162  ce0addcnnul  6180  ce0nnulb  6183  ncpw1pwneg  6202  sbthlem1  6204  sbth  6207  addlec  6209  nc0le1  6217  leconnnc  6219  addceq0  6220  dflec3  6222  lenc  6224  tc11  6229  taddc  6230  letc  6232  ce0t  6233  ce2le  6234  ce0lenc1  6240  addcdi  6251  muc0or  6253  0lt1c  6259  spacid  6286  nchoicelem9  6298  nchoicelem14  6303  nchoicelem17  6306  nchoicelem19  6308  frecsuc  6323  scancan  6332