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 124 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem is referenced by: sylan 281 vtocl2gf 2722 vtocl3gf 2723 vtoclegft 2732 sbcthdv 2896 disji2 3892 swopolem 4197 funssres 5135 fvmptssdm 5473 fmptcof 5555 fliftfuns 5667 isorel 5677 caovclg 5891 caovcomg 5894 caovassg 5897 caovcang 5900 caovordig 5904 caovordg 5906 caovdig 5913 caovdirg 5916 qliftfuns 6481 nneneq 6719 supmoti 6848 exmidonfinlem 7017 recexprlemopl 7401 recexprlemopu 7403 cauappcvgprlemladdrl 7433 caucvgsrlemcl 7565 caucvgsrlemfv 7567 caucvgsr 7578 suplocsrlempr 7583 ltordlem 8212 lble 8673 uz11 9316 seq3caopr3 10222 climcaucn 11088 sumdc 11095 fsum3 11124 fsumf1o 11127 fsum3cvg2 11131 isummulc2 11163 fsum2dlemstep 11171 fisumcom2 11175 fsumshftm 11182 fisum0diag2 11184 fsum00 11199 isumshft 11227 dvdsprm 11744 ssnei2 12253 psmet0 12423 psmettri2 12424 cncfi 12661 dvcn 12760 exmid1stab 13122 nninfsellemdc 13133 |
Copyright terms: Public domain | W3C validator |