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 926 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 119 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 919 |
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 921 |
This theorem is referenced by: 3adant2l 1163 3adant2r 1164 brelrng 4583 funimaexglem 5002 fvun2 5261 nnaordi 6104 nnmword 6114 prcdnql 6674 prcunqu 6675 prarloc 6693 ltaprg 6809 mul12 7237 add12 7266 addsub 7319 addsubeq4 7323 ppncan 7350 leadd1 7534 ltaddsub2 7541 leaddsub2 7543 lemul1 7693 reapmul1lem 7694 reapadd1 7696 reapcotr 7698 remulext1 7699 div23ap 7779 ltmulgt11 7942 lediv1 7947 lemuldiv 7959 zdiv 8435 iooneg 9010 icoshft 9012 fzaddel 9077 fzshftral 9125 facwordi 9667 abssubge0 9988 climshftlemg 10141 dvdsmul1 10217 divalgb 10325 lcmgcdeq 10465 |
Copyright terms: Public domain | W3C validator |