![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpan9 | GIF 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 2661 vtocl3gf 2662 vtoclegft 2671 sbcthdv 2830 swopolem 4068 funssres 4972 fvmptssdm 5287 fmptcof 5363 fliftfuns 5469 isorel 5479 caovclg 5684 caovcomg 5687 caovassg 5690 caovcang 5693 caovordig 5697 caovordg 5699 caovdig 5706 caovdirg 5709 qliftfuns 6256 nneneq 6392 supmoti 6465 recexprlemopl 6877 recexprlemopu 6879 cauappcvgprlemladdrl 6909 caucvgsrlemcl 7027 caucvgsrlemfv 7029 caucvgsr 7040 lble 8092 uz11 8722 iseqfeq 9547 iseqcaopr3 9556 climcaucn 10326 sumdc 10333 dvdsprm 10662 |
Copyright terms: Public domain | W3C validator |