![]() |
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 520 | . 2 ⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) ↔ ((φ ∧ ψ) ∧ (χ ∧ θ))) | |
2 | an4s.1 | . 2 ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ) | |
3 | 1, 2 | sylbi 114 | 1 ⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) → τ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
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 |
This theorem is referenced by: an42s 523 anandis 526 anandirs 527 trin2 4659 fnun 4948 2elresin 4953 f1co 5044 f1oun 5089 f1oco 5092 f1mpt 5353 poxp 5794 tfrlem7 5874 brecop 6132 th3qlem1 6144 oviec 6148 addcmpblnq 6351 mulcmpblnq 6352 mulpipqqs 6357 mulclnq 6360 mulcanenq 6369 distrnqg 6371 mulcmpblnq0 6427 mulcanenq0ec 6428 mulclnq0 6435 nqnq0a 6437 nqnq0m 6438 distrnq0 6442 genipv 6492 genpelvl 6495 genpelvu 6496 genpml 6500 genpmu 6501 genpcdl 6502 genpcuu 6503 genprndl 6504 genprndu 6505 distrlem1prl 6558 distrlem1pru 6559 ltsopr 6570 addcmpblnr 6667 ltsrprg 6675 addclsr 6681 mulclsr 6682 addasssrg 6684 addresr 6734 mulresr 6735 axaddass 6756 axmulass 6757 axdistr 6758 mulgt0 6890 mul4 6942 add4 6969 2addsub 7022 addsubeq4 7023 sub4 7052 muladd 7177 mulsub 7194 add20i 7279 mulge0i 7404 mulap0b 7418 divmuldivap 7470 ltmul12a 7607 zmulcl 8073 uz2mulcl 8321 qaddcl 8346 qmulcl 8348 qreccl 8351 rpaddcl 8381 ge0addcl 8620 expge1 8946 bj-indind 9391 |
Copyright terms: Public domain | W3C validator |