Theorem mpi 21

Description: A nested modus ponens inference. Inference associated with com12 33. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Hypotheses

Ref	Expression
mpi.1	⊢ 𝜓
mpi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpi	⊢ (𝜑 → 𝜒)

Proof of Theorem mpi

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpd 16	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpisyl  22  syl6mpi  68  mp2ani  711  mp3an3  1479  merco2  1769  equs4v  2033  alequexv  2034  equcomiv  2047  equcomi  2050  equvinva  2063  aeveq  2091  spimt  2416  equs4  2446  axc15  2452  2ax6elem  2500  dfeumo  2562  mo4  2592  sbcth  3754  sbcth2  3831  ssun3  4126  ssun4  4127  vn0  4291  elpreqprlem  4826  uniintsn  4945  sepexlem  5254  axprlem2  5386  axprlem4  5388  axpr  5389  axprlem1OLD  5390  axprglem  5394  exel  5402  rext  5416  exss  5431  snopeqop  5478  propssopi  5480  uniopel  5489  opthhausdorff  5490  opthhausdorff0  5491  wefrc  5645  relopabi  5800  relop  5828  dmrnssfld  5956  iss  6027  sofld  6179  ordun  6469  funimass2  6623  fvbr0  6912  fvmptg  6991  funsndifnop  7155  ov3  7583  elovmpo  7666  dford5  7798  limsssuc  7861  tfisi  7870  finds1  7911  frxp  8138  frxp2  8161  frxp3  8168  dfrecs3  8380  tfrlem1  8383  oaordi  8554  oaword2  8561  omeulem1  8590  oeworde  8602  oelim2  8604  nnaordi  8627  oaabs2  8658  limenpsi  9171  dif1en  9177  ordunifi  9281  fidomdm  9323  dffi3  9423  oismo  9534  wdom2d  9574  wdomima2g  9580  epnsym  9610  suc11reg  9620  elom3  9649  cantnfval2  9670  rankunb  9864  rankval4  9884  karden  9959  kardenOLD  9960  cardsn  10050  cardlim  10053  cardprclem  10060  fseqdom  10105  dfac12lem3  10224  kmlem2  10230  kmlem10  10238  cflim2  10341  cfslb2n  10346  fin23lem27  10406  fin23lem17  10416  axcc3  10516  axcc4  10517  acncc  10518  domtriomlem  10520  axdclem2  10598  imadomg  10613  imadomnum  10614  alephval2  10657  alephreg  10667  axextnd  10676  fpwwe2lem9  10724  pwfseq  10749  gch2  10760  axgroth3  10916  inaprc  10921  nlt1pi  10991  indpi  10992  1re  11308  mul02lem2  11487  addrid  11490  fimaxre  12261  fiminre  12264  supaddc  12284  supmul1  12286  rimul  12311  nnge1  12366  zneo  12782  ltweuz  14104  hashrabsn1  14518  hashf1lem2  14601  hash2pwpr  14621  climuni  15719  fsum2d  15937  fsumabs  15968  fsumrlim  15978  fsumo1  15979  fsumiun  15988  fprod2d  16148  efne0d  16263  efne0OLD  16265  ruclem13  16410  dvdslelem  16479  mod2eq1n2dvds  16517  nn0o1gt2  16551  divalglem0  16563  lcmfnnval  16799  prmreclem2  17095  prmreclem3  17096  mreexexd  17822  coaval  18243  xpcco  18357  pltirr  18507  frgpnabllem1  20087  ablfac1eulem  20288  prmgrpsimpgd  20330  mdetunilem9  22935  mretopd  23410  fiuncmp  23722  ptcmpfi  24132  filtop  24174  supnfcls  24339  flimfnfcls  24347  alexsubALTlem2  24367  alexsubALTlem4  24369  trust  24548  rectbntr0  25152  fsumcn  25191  ovoliunlem3  25825  ovolicc2lem4  25841  dyadmax  25919  vitali  25934  itgfsum  26147  dvmptfsum  26295  fta1g  26488  fta1  26629  aannenlem1  26655  aalioulem3  26661  logltb  26928  logdmn0  26968  ang180lem2  27138  angpined  27158  mumullem2  27507  lgsqrmodndvds  27680  gausslemma2dlem0i  27691  2lgs  27734  dchrisum0re  27840  chpdifbnd  27882  pntrlog2bnd  27911  pntibndlem3  27919  pnt3  27939  nofv  28014  nomaxmo  28055  nominmo  28056  noprc  28142  madebday  28286  addsproplem7  28361  negsproplem7  28420  elons2  28644  nbgrval  29917  vtxdginducedm1fi  30125  upgrewlkle2  30187  hiidge0  31700  chsupval  31937  chsupcl  31942  chsupss  31944  ococin  32010  chsupval2  32012  ssjo  32049  h1de2i  32155  pjss2i  32282  pjssmii  32283  sto2i  32839  stge1i  32840  stle0i  32841  stlei  32842  stlesi  32843  stm1i  32845  staddi  32848  stadd3i  32850  golem1  32873  stcltrlem1  32878  mdexchi  32937  chirred  32997  atabsi  33003  abrexdomjm  33103  iocinif  33373  cycpmcl  33677  elrgspnsubrunlem2  33809  voliune  34862  volfiniune  34863  probdif  35052  bnj849  35555  axprALT2  35734  acwer1prclem  35759  acwer1prc  35760  onvf1odlem4  35885  onvf1od  35886  vonf1onprcf1ac  35894  onvfowev  35899  kur14lem9  35979  gonarlem  36159  gonar  36160  goalrlem  36161  goalr  36162  sscoid  36675  limsucncmpi  37233  axtco1from2  37263  axtcond  37266  bj-nnf-spime  37677  bj-axc10  37695  bj-alequex  37696  bj-spimtv  37706  bj-moeub  37761  bj-exlimvmpi  37823  bj-exlimmpi  37824  bj-restpw  38013  bj-isrvec  38215  finxpreclem4  38317  domalom  38327  wl-isseteq  38428  wl-embant  38442  wl-orel12  38443  wl-euequf  38506  poimirlem9  38547  dfprop2  38646  abrexdom  38664  heiborlem10  38754  dvrunz  38888  iss2  39276  equcomi1  39957  ax12eq  39998  ax12el  39999  ax12inda  40005  ax12v2-o  40006  cvrnrefN  40339  pmod1i  40905  pmodN  40907  osumcllem11N  41023  pexmidlem8N  41034  pl42lem3N  41038  cdleme18b  41349  dochexmidlem8  42524  imadomfi  43052  sticksstones3  43198  sn-axprlem3  43272  sn-exelALT  43273  sn-1ne2  43330  remul02  43456  sn-0tie0  43515  pellexlem3  43837  pell1234qrne0  43859  hbtlem6  44130  onsucelab  44264  omabs2  44333  nadd2rabex  44387  or3or  45022  isotone1  45047  isotone2  45048  clsf2  45125  ismnushort  45284  radcnvrat  45297  3impexpbicom  45462  sb5ALT  45507  eexinst01  45508  ax6e2eq  45539  sineq0ALT  45918  tcfr  45952  ssclaxsep  45971  omssaxinf2  45977  nregmodel  46006  fzisoeu  46315  ovnsubaddlem2  47580  ormklocald  47885  funressnfv  48112  faovcl  48269  sprsymrelfo  48578  clnbgrval  48919  gpgedgiov  49162  gpgedg2ov  49163  gpgedg2iv  49164  pgnioedg1  49205  pgnioedg2  49206  pgnioedg3  49207  pgnioedg4  49208  pgnioedg5  49209  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  pgnbgreunbgrlem5lem1  49217  pgnbgreunbgrlem5lem2  49218  cznnring  49358  zlmodzxznm  49608  elbigolo1  49668  dignn0flhalflem1  49726  nn0sumshdig  49734  rrx2xpref1o  49829  fonex  49976  vsetrec  50795