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 980 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 973 |
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 975 |
This theorem is referenced by: 3adant2l 1227 3adant2r 1228 brelrng 4842 iotam 5190 funimaexglem 5281 fvun2 5563 nnaordi 6487 nnmword 6497 fpmg 6652 prcdnql 7446 prcunqu 7447 prarloc 7465 ltaprg 7581 mul12 8048 add12 8077 addsub 8130 addsubeq4 8134 ppncan 8161 leadd1 8349 ltaddsub2 8356 leaddsub2 8358 lemul1 8512 reapmul1lem 8513 reapadd1 8515 reapcotr 8517 remulext1 8518 div23ap 8608 ltmulgt11 8780 lediv1 8785 lemuldiv 8797 zdiv 9300 iooneg 9945 icoshft 9947 fzaddel 10015 fzshftral 10064 facwordi 10674 abssubge0 11066 climshftlemg 11265 dvdsmul1 11775 divalgb 11884 lcmgcdeq 12037 pcfac 12302 cnmptcom 13092 hmeof1o2 13102 |
Copyright terms: Public domain | W3C validator |