Theorem mpbi 145

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbi.min	⊢ 𝜑
mpbi.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbi	⊢ 𝜓

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 ⊢ 𝜑
2		mpbi.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpi 120	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74i  180  pm4.71i  391  pm4.71ri  392  pm5.32i  454  biadanii  615  pm3.24  698  olc  716  orc  717  dcnn  853  dn1dc  966  3ori  1334  mptxor  1466  mpgbi  1498  dveeq2  1861  dveeq2or  1862  sbequilem  1884  nfsb  1997  sbco  2019  sbcocom  2021  hbsbd  2033  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  hbe1a  2074  elsb1  2207  elsb2  2208  eqcomi  2233  eqtri  2250  eleqtri  2304  neii  2402  neeqtri  2427  nesymi  2446  necomi  2485  nemtbir  2489  neli  2497  nrex  2622  rexlimi  2641  isseti  2808  eueq1  2975  euxfr2dc  2988  cdeqri  3014  sseqtri  3258  3sstr3i  3264  equncomi  3350  unssi  3379  ssini  3427  unabs  3435  inabs  3436  ddifss  3442  inssddif  3445  snid  3697  rabrsndc  3734  rintm  4058  breqtri  4108  bm1.3ii  4205  zfnuleu  4208  zfpow  4260  undifexmid  4278  copsexg  4331  uniop  4343  pwundifss  4377  onunisuci  4524  zfun  4526  op1stb  4570  op1stbg  4571  ordtriexmidlem  4612  ordtriexmid  4614  ordtri2orexmid  4616  2ordpr  4617  ontr2exmid  4618  onsucsssucexmid  4620  onsucelsucexmid  4623  dtruex  4652  ordsoexmid  4655  0elsucexmid  4658  ordtri2or2exmid  4664  dcextest  4674  tfi  4675  relop  4875  dmxpid  4948  rn0  4983  dmresi  5063  issref  5114  cnvcnv  5184  rescnvcnv  5194  cnvcnvres  5195  cnvsn  5214  cocnvcnv2  5243  cores2  5244  co01  5246  relcoi1  5263  cnviinm  5273  fnopab  5451  mpt0  5454  fnmpti  5455  f1cnvcnv  5547  f1ovi  5617  fmpti  5792  fvsnun2  5844  oprabss  6099  relmptopab  6216  2nd0  6300  f1stres  6314  f2ndres  6315  reldmtpos  6410  dftpos4  6420  tpostpos  6421  tpos0  6431  smo0  6455  frecfnom  6558  oasuc  6623  uniixp  6881  ssdomg  6943  xpcomf1o  6997  ssfilem  7050  diffitest  7062  inffiexmid  7084  fiintim  7109  caseinl  7274  caseinr  7275  eninl  7280  eninr  7281  card0  7376  dju1p1e2  7391  pw1on  7427  dmaddpi  7528  dmmulpi  7529  1lt2pi  7543  1lt2nq  7609  suplocsrlempr  8010  gtso  8241  subf  8364  negne0i  8437  negdii  8446  ltapii  8798  sup3exmid  9120  neg1ap0  9235  halflt1  9344  nn0ssz  9480  3halfnz  9560  zeo  9568  numlt  9618  numltc  9619  le9lt10  9620  decle  9627  uzf  9741  indstr  9805  infrenegsupex  9806  xaddf  10057  ixxf  10111  iooval2  10128  ioof  10184  unirnioo  10186  fzval2  10224  fzf  10225  fz10  10259  fzpreddisj  10284  4fvwrd4  10353  fzof  10357  fldiv4p1lem1div2  10542  fldiv4lem1div2  10544  xnn0nnen  10676  sqrt2gt1lt2  11581  infxrnegsupex  11795  fclim  11826  fsumrelem  12003  arisum2  12031  geo2sum2  12047  0.999...  12053  ege2le3  12203  sin0  12261  ef01bndlem  12288  cos2bnd  12292  cos01gt0  12295  sincos2sgn  12298  sin4lt0  12299  egt2lt3  12312  n2dvds1  12444  flodddiv4  12468  0bits  12491  gcdf  12514  nninfct  12583  eucalgf  12598  2prm  12670  dfphi2  12763  pockthi  12902  karatsuba  12974  znnen  12990  ennnfonelem1  12999  qnnen  13023  ctiunct  13032  ssnnctlemct  13038  structcnvcnv  13069  structfn  13072  relelbasov  13116  xpsff1o  13403  rmodislmod  14336  cnfld0  14556  cnfld1  14557  eltpsi  14736  unitg  14757  epttop  14785  txuni2  14951  retopon  15221  cnfldtopon  15235  dedekindicclemicc  15327  reldvg  15374  dvrecap  15408  dvef  15422  plyrecj  15458  sinhalfpilem  15486  coseq00topi  15530  coseq0negpitopi  15531  sincos4thpi  15535  sincos6thpi  15537  pigt3  15539  cos02pilt1  15546  logltb  15569  rpabscxpbnd  15635  sgmf  15681  1sgm2ppw  15690  lgsdir2lem2  15729  lgsdir2lem3  15730  ex-fl  16198  ex-exp  16200  bdceqi  16315  bdcriota  16355  bdsepnfALT  16361  bdbm1.3ii  16363  bj-d0clsepcl  16397  nninfsellemeqinf  16496