![]() |
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 586 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | |
2 | an4s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
3 | 1, 2 | sylbi 121 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: an42s 589 anandis 592 anandirs 593 trin2 5038 fnun 5341 2elresin 5346 f1co 5452 f1oun 5500 f1oco 5503 f1mpt 5793 poxp 6257 tfrlem7 6342 brecop 6651 th3qlem1 6663 oviec 6667 pmss12g 6701 addcmpblnq 7396 mulcmpblnq 7397 mulpipqqs 7402 mulclnq 7405 mulcanenq 7414 distrnqg 7416 mulcmpblnq0 7473 mulcanenq0ec 7474 mulclnq0 7481 nqnq0a 7483 nqnq0m 7484 distrnq0 7488 genipv 7538 genpelvl 7541 genpelvu 7542 genpml 7546 genpmu 7547 genpcdl 7548 genpcuu 7549 genprndl 7550 genprndu 7551 distrlem1prl 7611 distrlem1pru 7612 ltsopr 7625 addcmpblnr 7768 ltsrprg 7776 addclsr 7782 mulclsr 7783 addasssrg 7785 addresr 7866 mulresr 7867 axaddass 7901 axmulass 7902 axdistr 7903 mulgt0 8062 mul4 8119 add4 8148 2addsub 8201 addsubeq4 8202 sub4 8232 muladd 8371 mulsub 8388 add20i 8479 mulge0i 8607 mulap0b 8642 divmuldivap 8699 ltmul12a 8847 zmulcl 9336 uz2mulcl 9638 qaddcl 9665 qmulcl 9667 qreccl 9672 rpaddcl 9707 ge0addcl 10011 ge0xaddcl 10013 expge1 10588 rexanuz 11029 amgm2 11159 iooinsup 11317 mulcn2 11352 dvds2ln 11863 opoe 11932 omoe 11933 opeo 11934 omeo 11935 lcmgcd 12110 lcmdvds 12111 pc2dvds 12362 tgcl 14024 innei 14123 txbas 14218 txss12 14226 txbasval 14227 blsscls2 14453 qtopbasss 14481 lgslem3 14864 bj-indind 15145 |
Copyright terms: Public domain | W3C validator |