Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syldan | GIF version |
Description: A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.) |
Ref | Expression |
---|---|
syldan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
syldan.2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
syldan | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syldan.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | syldan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
3 | 2 | expcom 109 | . . 3 ⊢ (𝜒 → (𝜑 → 𝜃)) |
4 | 3 | adantrd 264 | . 2 ⊢ (𝜒 → ((𝜑 ∧ 𝜓) → 𝜃)) |
5 | 1, 4 | mpcom 32 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia3 101 |
This theorem is referenced by: sylan2 270 dn1dc 867 stoic2a 1318 sbcied2 2800 csbied2 2893 elpw2g 3910 pofun 4049 tfi 4305 fnbr 5001 caovlem2d 5693 grprinvlem 5695 caofcom 5734 fnexALT 5740 tfri3 5953 f1domg 6238 archnqq 6515 nqpru 6650 ltaddpr 6695 1idsr 6853 addgt0sr 6860 gt0ap0 7616 ap0gt0 7629 mulgt1 7829 gt0div 7836 ge0div 7837 ltdiv2 7853 creur 7911 avgle1 8165 recnz 8333 qreccl 8576 xrrege0 8738 peano2fzor 9088 flqltnz 9129 flqdiv 9163 frecuzrdgfn 9198 frecuzrdgcl 9199 frecuzrdgsuc 9201 iseqfveq 9230 isermono 9237 iseqsplit 9238 iseqid 9247 le2sq2 9329 caucvgrelemcau 9579 caucvgre 9580 r19.2uz 9591 sqrtgt0 9632 clim2iser 9857 clim2iser2 9858 climub 9864 serif0 9871 ialgfx 9891 |
Copyright terms: Public domain | W3C validator |