| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3com12 | Structured version Visualization version GIF version | ||
| Description: Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
| Ref | Expression |
|---|---|
| 3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| 3com12 | ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 2 | 1 | 3exp 1120 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| 3 | 2 | 3imp21 1114 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 3comr 1126 3com23 1127 brelrng 5952 fnunres2 6681 fresaunres1 6781 fvun2 7001 onfununi 8381 oaword 8587 nnaword 8665 nnmword 8671 naddel1 8725 naddss1 8727 ecopovtrn 8860 fpmg 8908 tskord 10820 ltadd2 11365 mul12 11426 add12 11479 addsub 11519 addsubeq4 11523 ppncan 11551 leadd1 11731 ltaddsub2 11738 leaddsub2 11740 ltsub1 11759 ltsub2 11760 div23 11941 ltmul1 12117 ltmulgt11 12127 lediv1 12133 lemuldiv 12148 ltdiv2 12154 zdiv 12688 xltadd1 13298 xltmul1 13334 iooneg 13511 icoshft 13513 fzaddel 13598 fzshftral 13655 modmulmodr 13978 facwordi 14328 pfxeq 14734 abssubge0 15366 climshftlem 15610 dvdsmul1 16315 divalglem8 16437 divalgb 16441 rprpwr 16596 lcmgcdeq 16649 pcfac 16937 mhmmulg 19133 rmodislmodlem 20927 xrsdsreval 21429 cnmptcom 23686 hmeof1o2 23771 ordthmeo 23810 isclmi0 25131 iscvsi 25162 cxplt2 26740 sleadd1im 28020 sltadd2 28024 addscan2 28026 axcontlem8 28986 vcdi 30584 isvciOLD 30599 dipdi 30862 dipsubdi 30868 hvadd12 31054 hvmulcom 31062 his5 31105 bcs3 31202 chj12 31553 spansnmul 31583 homul12 31824 hoaddsub 31835 lnopmul 31986 lnopaddmuli 31992 lnopsubmuli 31994 lnfnaddmuli 32064 leop2 32143 dmdsl3 32334 chirredlem3 32411 atmd2 32419 cdj3lem3 32457 signstfvc 34589 3com12d 36311 cnambfre 37675 sdclem2 37749 indstrd 42194 addrcom 44494 uun123p1 44829 sineq0ALT 44957 stoweidlem17 46032 sigaras 46870 sigarms 46871 i0oii 48817 |
| Copyright terms: Public domain | W3C validator |