![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3expa | GIF version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((φ ∧ ψ ∧ χ) → θ) |
Ref | Expression |
---|---|
3expa | ⊢ (((φ ∧ ψ) ∧ χ) → θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((φ ∧ ψ ∧ χ) → θ) | |
2 | 1 | 3exp 1102 | . 2 ⊢ (φ → (ψ → (χ → θ))) |
3 | 2 | imp31 243 | 1 ⊢ (((φ ∧ ψ) ∧ χ) → θ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 884 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 886 |
This theorem is referenced by: 3anidm23 1193 mp3an2 1219 mpd3an3 1232 rgen3 2400 moi2 2716 sbc3ie 2825 preq12bg 3535 issod 4047 reuhypd 4169 funimass4 5167 fvtp1g 5312 f1imass 5356 fcof1o 5372 f1ofveu 5443 f1ocnvfv3 5444 acexmid 5454 2ndrn 5751 rdgon 5913 frecrdg 5931 ltapig 6322 ltanqi 6386 ltmnqi 6387 lt2addnq 6388 prarloclemcalc 6485 genpassl 6507 genpassu 6508 prmuloc 6547 ltexprlemm 6574 ltexprlemfl 6583 ltexprlemfu 6585 ltaprg 6592 mul4 6942 add4 6969 cnegexlem2 6984 cnegexlem3 6985 2addsub 7022 addsubeq4 7023 muladd 7177 ltleadd 7236 reapmul1 7379 apreim 7387 receuap 7432 p1le 7596 lemul12b 7608 zdiv 8104 fzind 8129 fnn0ind 8130 uzss 8269 qmulcl 8348 qreccl 8351 xrlttr 8486 icc0r 8565 iooshf 8591 elfz5 8652 elfz0fzfz0 8753 fzind2 8865 expnegap0 8917 expineg2 8918 mulexpzap 8949 expsubap 8956 expnbnd 9025 crim 9086 |
Copyright terms: Public domain | W3C validator |