# Metamath Proof Explorer

## Axiom ax-frege2

Description: If a proposition ch is a necessary consequence of two propositions ps and ph and one of those, ps , is in turn a necessary consequence of the other, ph , then the proposition ch is a necessary consequence of the latter one, ph , alone. Axiom 2 of Frege1879 p. 26. Identical to ax-2 . (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

Ref Expression
Assertion ax-frege2 ${⊢}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\phi }\to {\chi }\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 wph ${wff}{\phi }$
1 wps ${wff}{\psi }$
2 wch ${wff}{\chi }$
3 1 2 wi ${wff}\left({\psi }\to {\chi }\right)$
4 0 3 wi ${wff}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
5 0 1 wi ${wff}\left({\phi }\to {\psi }\right)$
6 0 2 wi ${wff}\left({\phi }\to {\chi }\right)$
7 5 6 wi ${wff}\left(\left({\phi }\to {\psi }\right)\to \left({\phi }\to {\chi }\right)\right)$
8 4 7 wi ${wff}\left(\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\left({\phi }\to {\psi }\right)\to \left({\phi }\to {\chi }\right)\right)\right)$