![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3com12 | GIF version |
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3com12 | ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma 927 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 119 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: 3adant2l 1164 3adant2r 1165 brelrng 4587 funimaexglem 5007 fvun2 5266 nnaordi 6140 nnmword 6150 prcdnql 6725 prcunqu 6726 prarloc 6744 ltaprg 6860 mul12 7293 add12 7322 addsub 7375 addsubeq4 7379 ppncan 7406 leadd1 7590 ltaddsub2 7597 leaddsub2 7599 lemul1 7749 reapmul1lem 7750 reapadd1 7752 reapcotr 7754 remulext1 7755 div23ap 7835 ltmulgt11 7998 lediv1 8003 lemuldiv 8015 zdiv 8505 iooneg 9075 icoshft 9077 fzaddel 9142 fzshftral 9190 facwordi 9753 abssubge0 10115 climshftlemg 10268 dvdsmul1 10351 divalgb 10458 lcmgcdeq 10598 |
Copyright terms: Public domain | W3C validator |