![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > an42s | GIF version |
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
an41r3s.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
an42s | ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an41r3s.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
2 | 1 | an4s 578 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
3 | 2 | ancom2s 556 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nnmsucr 6392 ecopoveq 6532 enqdc 7193 addcmpblnq 7199 addpipqqslem 7201 addpipqqs 7202 addclnq 7207 addcomnqg 7213 distrnqg 7219 recexnq 7222 ltdcnq 7229 ltexnqq 7240 enq0enq 7263 enq0sym 7264 enq0breq 7268 addclnq0 7283 distrnq0 7291 mulclsr 7586 axmulass 7705 axdistr 7706 subadd4 8030 mulsub 8187 tgcl 12272 |
Copyright terms: Public domain | W3C validator |