![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > an4s | GIF version |
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
an4s.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
an4s | ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an4 556 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | |
2 | an4s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: an42s 559 anandis 562 anandirs 563 trin2 4866 fnun 5165 2elresin 5170 f1co 5276 f1oun 5321 f1oco 5324 f1mpt 5604 poxp 6059 tfrlem7 6144 brecop 6449 th3qlem1 6461 oviec 6465 pmss12g 6499 addcmpblnq 7076 mulcmpblnq 7077 mulpipqqs 7082 mulclnq 7085 mulcanenq 7094 distrnqg 7096 mulcmpblnq0 7153 mulcanenq0ec 7154 mulclnq0 7161 nqnq0a 7163 nqnq0m 7164 distrnq0 7168 genipv 7218 genpelvl 7221 genpelvu 7222 genpml 7226 genpmu 7227 genpcdl 7228 genpcuu 7229 genprndl 7230 genprndu 7231 distrlem1prl 7291 distrlem1pru 7292 ltsopr 7305 addcmpblnr 7435 ltsrprg 7443 addclsr 7449 mulclsr 7450 addasssrg 7452 addresr 7524 mulresr 7525 axaddass 7557 axmulass 7558 axdistr 7559 mulgt0 7710 mul4 7765 add4 7794 2addsub 7847 addsubeq4 7848 sub4 7878 muladd 8013 mulsub 8030 add20i 8121 mulge0i 8248 mulap0b 8277 divmuldivap 8333 ltmul12a 8476 zmulcl 8959 uz2mulcl 9252 qaddcl 9277 qmulcl 9279 qreccl 9284 rpaddcl 9314 ge0addcl 9605 ge0xaddcl 9607 expge1 10171 rexanuz 10600 amgm2 10730 iooinsup 10885 mulcn2 10920 dvds2ln 11321 opoe 11387 omoe 11388 opeo 11389 omeo 11390 lcmgcd 11552 lcmdvds 11553 tgcl 12015 innei 12114 txbas 12208 txss12 12216 txbasval 12217 blsscls2 12421 qtopbasss 12443 bj-indind 12715 |
Copyright terms: Public domain | W3C validator |