![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE 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 set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com3r 73 com13 74 pm2.04 76 pm2.86d 93 impancom 247 con2d 554 impidc 754 pm2.61dc 761 3com23 1109 expcomd 1327 spimth 1620 sbiedh 1667 eqrdav 2036 necon4bbiddc 2273 ralrimdva 2393 ralrimdvva 2398 ceqsalt 2574 vtoclgft 2598 reu6 2724 sbciegft 2787 reuss2 3211 reupick 3215 reusv3 4158 ssrel 4371 ssrel2 4373 ssrelrel 4383 funssres 4885 funcnvuni 4911 fv3 5140 fvmptt 5205 funfvima2 5334 isoini 5400 isopolem 5404 f1ocnv2d 5646 f1o2ndf1 5791 nnmordi 6025 nnmord 6026 xpdom2 6241 genpcdl 6502 genpcuu 6503 distrlem5prl 6562 distrlem5pru 6563 lemul12a 7609 divgt0 7619 divge0 7620 bndndx 7956 elnnz 8031 fzind 8129 fnn0ind 8130 eqreznegel 8325 lbzbi 8327 irradd 8355 irrmul 8356 iccid 8564 uzsubsubfz 8681 fzrevral 8737 elfz0fzfz0 8753 fz0fzelfz0 8754 elfzmlbp 8760 elfzodifsumelfzo 8827 ssfzo12bi 8851 elfzonelfzo 8856 le2sq2 8982 bj-rspgt 9260 |
Copyright terms: Public domain | W3C validator |