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 969 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: 3adant2l 1210 3adant2r 1211 brelrng 4765 funimaexglem 5201 fvun2 5481 nnaordi 6397 nnmword 6407 fpmg 6561 prcdnql 7285 prcunqu 7286 prarloc 7304 ltaprg 7420 mul12 7884 add12 7913 addsub 7966 addsubeq4 7970 ppncan 7997 leadd1 8185 ltaddsub2 8192 leaddsub2 8194 lemul1 8348 reapmul1lem 8349 reapadd1 8351 reapcotr 8353 remulext1 8354 div23ap 8444 ltmulgt11 8615 lediv1 8620 lemuldiv 8632 zdiv 9132 iooneg 9764 icoshft 9766 fzaddel 9832 fzshftral 9881 facwordi 10479 abssubge0 10867 climshftlemg 11064 dvdsmul1 11504 divalgb 11611 lcmgcdeq 11753 cnmptcom 12456 hmeof1o2 12466 |
Copyright terms: Public domain | W3C validator |