Theorem mpi 44

Description: A nested modus ponens inference. (The proof was 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 8	. 2 ⊢ (φ → ψ)
3		mpi.2	. 2 ⊢ (φ → (ψ → χ))
4	2, 3	mpd 26	1 ⊢ (φ → χ)

Syntax hints:   → wi 3

This theorem is referenced by:  mpii 45  mtoi 107  mt2i 110  mt3i 113  mpbii 193  mpbiri 194  mpan2 695  mpani 697  mp2ani 699  mt2bi 712  ax4 971  ax9o 1121  equcomi 1127  equvini 1167  ax11v2 1214  ax16i 1269  ax11eq 1362  ax11el 1363  ax11inda 1370  a12stdy1 1371  a12study 1377  ceqsex 1831  moeq3 1918  sbcth 1943  ssun3 2192  ssun4 2193  ssin 2229  ralf0 2356  prss 2468  tpss 2473  dtruALT 2744  rext 2750  exss 2765  uniopel 2805  wefrc 2939  suceloni 3058  ordun 3077  limsssuc 3117  snsn0non 3121  finds1 3155  relop 3271  dmrnssfld 3353  iss 3393  cotr 3432  cnvsym 3433  coexg 3520  nfunv 3542  funimass2 3569  fvopab4g 3774  funfvop 3798  canth 3902  foprcl 4010  oprabval2gf 4021  oaordi 4173  oaword2 4180  oeworde 4213  oelim2 4215  ecelqsi 4285  enrefg 4380  xpdom2 4431  sbthlem1 4436  mapdom2 4483  limenpsi 4494  onomeneq 4507  suc11reg 4588  infeq5 4604  elom3 4614  r1val1 4641  rankwflem 4648  rankr1 4657  rankel 4663  rankpw 4667  r1pwcl 4670  rankun 4674  rankval4 4685  karden 4709  kmlem2 4749  kmlem10 4757  zorn2lem7 4777  imadomg 4789  unidom 4791  carden 4814  cardsn 4817  carddomi 4818  sdomsdomcard 4831  cardlim 4834  cardiun 4842  alephfplem3 4881  alephval2 4885  axextnd 4926  nlt1pi 5016  indpi 5017  reclem3pr 5141  cnegext 5331  eqneg 5770  nnge1t 5901  elnnz1 6112  uzindOLD 6166  inelr 6680  abslt 6825  absle 6826  absltOLD 6827  absleOLD 6828  cvgratlem1ALT 7199  ivthlem3 7235  infcda 7527  infdif 7528  infxp 7532  infmap2lem2 7540  ghgrpilem1 8097  spwval2 8610  logltbt 8731  axgroth3 8734  grothinf 8736  hiidge0t 8919  ococint 9252  chsupval2t 9257  chsupvalt 9258  chsupclt 9263  chsupss 9265  shlej1 9303  h1de2 9431  pjss2 9582  pjssm 9583  sto2 10120  stge1 10121  stle0 10122  stle 10123  stles 10124  stm1 10126  stadd 10129  stadd3 10131  strlem6 10139  golem1 10154  stcltrlem1 10159  mdexch 10218  hatomistic 10245  irredt 10278  atabs 10284  filintf 10502  cnfilca 10510  rcfpfil 10517  dtt2 10534

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain