New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > com23 | GIF version |
Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.) |
Ref | Expression |
---|---|
com3.1 | ⊢ (φ → (ψ → (χ → θ))) |
Ref | Expression |
---|---|
com23 | ⊢ (φ → (χ → (ψ → θ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com3.1 | . 2 ⊢ (φ → (ψ → (χ → θ))) | |
2 | pm2.27 35 | . 2 ⊢ (χ → ((χ → θ) → θ)) | |
3 | 1, 2 | syl9 66 | 1 ⊢ (φ → (χ → (ψ → θ))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: com3r 73 com13 74 pm2.04 76 pm2.86d 93 impancom 427 dedlem0b 919 3com23 1157 exp3acom23 1372 ax12b 1689 a16g 1945 cbv1h 1978 sbied 2036 sbequi 2059 ax11indn 2195 eqrdav 2352 ralrimdva 2704 ralrimdvva 2709 ceqsalt 2881 vtoclgft 2905 reu6 3025 sbciegft 3076 reuss2 3535 reupick 3539 nnsucelr 4428 nndisjeq 4429 ltfintri 4466 ssfin 4470 evenodddisj 4516 nnadjoin 4520 sfintfin 4532 tfinnn 4534 spfinsfincl 4539 funssres 5144 funcnvuni 5161 fv3 5341 tz6.12-1 5344 funfvima2 5460 isoini 5497 f1o2d 5727 fnpprod 5843 enpw1 6062 enprmaplem3 6078 nclenn 6249 nchoicelem6 6294 nchoicelem12 6300 nchoicelem17 6305 |
Copyright terms: Public domain | W3C validator |