Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpan9 | Unicode version |
Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
mpan9.1 | |
mpan9.2 |
Ref | Expression |
---|---|
mpan9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpan9.1 | . . 3 | |
2 | mpan9.2 | . . 3 | |
3 | 1, 2 | syl5 32 | . 2 |
4 | 3 | impcom 123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 |
This theorem is referenced by: sylan 277 vtocl2gf 2660 vtocl3gf 2661 vtoclegft 2670 sbcthdv 2829 swopolem 4060 funssres 4962 fvmptssdm 5276 fmptcof 5352 fliftfuns 5458 isorel 5468 caovclg 5673 caovcomg 5676 caovassg 5679 caovcang 5682 caovordig 5686 caovordg 5688 caovdig 5695 caovdirg 5698 qliftfuns 6213 nneneq 6343 supmoti 6406 recexprlemopl 6815 recexprlemopu 6817 cauappcvgprlemladdrl 6847 caucvgsrlemcl 6965 caucvgsrlemfv 6967 caucvgsr 6978 lble 8025 uz11 8641 iseqfeq 9451 iseqcaopr3 9460 climcaucn 10188 dvdsprm 10518 |
Copyright terms: Public domain | W3C validator |