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	⊢ 𝜒
mpbiri.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbiri	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 ⊢ 𝜒
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
3		mpbiri.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbird 167	1 ⊢ (𝜑 → 𝜓)

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  1427  ceqsexv2d  2840  dedhb  2972  sbceqal  3084  ssdifeq0  3574  pwidg  3663  elpr2  3688  snidg  3695  exsnrex  3708  rabrsndc  3734  prid1g  3770  tpid1g  3779  tpid2g  3781  sssnr  3831  ssprr  3834  sstpr  3835  preqr1  3846  unimax  3922  intmin3  3950  eqbrtrdi  4122  pwnss  4244  0inp0  4251  bnd2  4258  ss1o0el1  4282  exmidsssn  4287  exmidundif  4291  exmidundifim  4292  euabex  4312  copsexg  4331  euotd  4342  elopab  4347  epelg  4382  sucidg  4508  ifelpwung  4573  regexmidlem1  4626  sucprcreg  4642  onprc  4645  dtruex  4652  omelon2  4701  elvvuni  4785  eqrelriv  4814  relopabi  4850  opabid2  4856  ididg  4878  iss  5054  funopg  5355  fn0  5446  f00  5522  f0bi  5523  f10d  5612  f1o00  5613  fo00  5614  brprcneu  5625  relelfvdm  5664  fvmbr  5667  fsn  5812  funop  5823  eufnfv  5877  f1eqcocnv  5924  riotaprop  5989  acexmidlemb  6002  acexmidlemab  6004  acexmidlem2  6007  oprabid  6042  elrnmpo  6127  ov6g  6152  eqop2  6333  1stconst  6378  2ndconst  6379  dftpos3  6419  dftpos4  6420  2pwuninelg  6440  frecabcl  6556  el2oss1o  6602  ecopover  6793  map0g  6848  mapsn  6850  elixpsn  6895  en0  6960  en1  6964  fiprc  6981  en2m  6987  dom0  7012  nneneq  7031  findcard  7063  findcard2  7064  findcard2s  7065  elssdc  7080  eqsndc  7081  sbthlem2  7141  sbthlemi4  7143  sbthlemi5  7144  eldju2ndl  7255  updjudhf  7262  enumct  7298  nnnninf  7309  nninfisollem0  7313  fodjuomnilemdc  7327  exmidonfinlem  7387  exmidaclem  7406  pw1ne1  7430  pw1ne3  7431  1ne0sr  7969  00sr  7972  cnm  8035  eqlei2  8257  cnstab  8808  divcanap3  8861  sup3exmid  9120  nn1suc  9145  nn0ge0  9410  xnn0xr  9453  xnn0nemnf  9459  elnn0z  9475  nn0n0n1ge2b  9542  nn0ind-raph  9580  elnn1uz2  9819  indstr2  9821  xrnemnf  9990  xrnepnf  9991  mnfltxr  9999  nn0pnfge0  10004  xrlttr  10008  xrltso  10009  xrlttri3  10010  nltpnft  10027  npnflt  10028  ngtmnft  10030  nmnfgt  10031  xsubge0  10094  xposdif  10095  xleaddadd  10100  fztpval  10296  fseq1p1m1  10307  fz01or  10324  qbtwnxr  10494  xqltnle  10504  fzfig  10669  uzsinds  10683  ser0f  10773  1exp  10807  0exp  10813  bcn1  10997  zfz1iso  11081  hash2en  11083  0wrd0  11115  wrdlen1  11127  wrdl1exs1  11182  swrdspsleq  11220  cats1un  11274  wrdind  11275  wrd2ind  11276  sqrt0rlem  11535  prodf1f  12075  0dvds  12343  nn0o  12439  flodddiv4  12468  bitsp1o  12485  gcddvds  12505  bezoutlemmain  12540  lcmdvds  12622  rpdvds  12642  1nprm  12657  prmind2  12663  nnoddn2prmb  12806  pcpre1  12836  qexpz  12896  4sqlem19  12953  ennnfonelemj0  12993  ennnfonelemhf1o  13005  strslfv  13098  restsspw  13303  xpsfrnel  13398  mgmidcl  13432  mgmlrid  13433  releqgg  13778  islidlm  14464  zrhrhm  14608  psrplusgg  14663  baspartn  14745  eltg3  14752  topnex  14781  discld  14831  cnpfval  14890  cnprcl2k  14901  idcn  14907  xmet0  15058  blfvalps  15080  blfps  15104  blf  15105  limcimolemlt  15359  recnprss  15382  lgsdir2lem2  15729  gausslemma2dlem4  15764  2lgslem2  15792  2lgslem3  15801  2lgs  15804  2sqlem7  15821  uhgr0e  15903  incistruhgr  15911  clwwlkn1  16186  funmptd  16276  bj-om  16409  bj-nn0suc0  16422  bj-nn0suc  16436  bj-nn0sucALT  16450  bj-findis  16451  2omap  16472  pw1map  16474  nninfall  16489  nnnninfen  16501  trilpolemcl  16519  dceqnconst  16542  dcapnconst  16543