mpan9 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > mpan9		Unicode version

Theorem mpan9 455

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

**Hypotheses**
Ref	Expression
mpan9.1
mpan9.2

**Assertion**
Ref	Expression
mpan9	$/\$

**Proof of Theorem mpan9**
Step	Hyp	Ref	Expression
1		mpan9.1	. . 3
2		mpan9.2	. . 3
3	1, 2	syl5 28	. 2
4	3	impcom 419	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 358

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8

This theorem depends on definitions: df-bi 177 df-an 360

This theorem is referenced by: sylan 457 vtocl2gf 2916 vtocl3gf 2917 vtoclegft 2926 sbcthdv 3061 nnsucelr 4428 nnadjoin 4520 sfintfin 4532 funiunfv 5467 isorel 5489 caovcld 5622 caovcomg 5624 caovassg 5626 caovdig 5632 caovdirg 5633