Theorem imim12d 29

Description: Deduction combining antecedents and consequents.

Hypotheses

Ref	Expression
imim12d.1	⊢ (φ → (ψ → χ))
imim12d.2	⊢ (φ → (θ → τ))

Assertion

Ref	Expression
imim12d	⊢ (φ → ((χ → θ) → (ψ → τ)))

Proof of Theorem imim12d

Step	Hyp	Ref	Expression
1		imim12d.1	. . 3 ⊢ (φ → (ψ → χ))
2	1	imim1d 28	. 2 ⊢ (φ → ((χ → θ) → (ψ → θ)))
3		imim12d.2	. . 3 ⊢ (φ → (θ → τ))
4	3	imim2d 25	. 2 ⊢ (φ → ((ψ → θ) → (ψ → τ)))
5	2, 4	syld 27	1 ⊢ (φ → ((χ → θ) → (ψ → τ)))

Syntax hints:   → wi 3

This theorem is referenced by:  pm3.48 556  a12lem1 1374  mo 1391  peano5 3153  tfrlem1 3913  dfuz 6170  uzindOLD 6176  fsump1s 6971  fsumcmp 6998  fsumcmpndx2 7000  climconst 7051  caucvglem5 7117  caucvglem6 7118  fsum0diaglem2 7212  clsval2 7647  cnpco 7731  cncnplem4 7739  metreslem 7786  metcnpi3 7856  metcnpi4 7857  metcni2 7859  metcnp4 7932  xpcn 7938  lmcau 7958  dmdmdt 10200  mdsl0 10208  mdsl1 10219  ghomf1olem 10364

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

Copyright terms: Public domain