ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  an42s GIF version

Theorem an42s 589
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an41r3s.1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
an42s (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)

Proof of Theorem an42s
StepHypRef Expression
1 an41r3s.1 . . 3 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
21an4s 588 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 566 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:  nnmsucr  6489  ecopoveq  6630  enqdc  7360  addcmpblnq  7366  addpipqqslem  7368  addpipqqs  7369  addclnq  7374  addcomnqg  7380  distrnqg  7386  recexnq  7389  ltdcnq  7396  ltexnqq  7407  enq0enq  7430  enq0sym  7431  enq0breq  7435  addclnq0  7450  distrnq0  7458  mulclsr  7753  axmulass  7872  axdistr  7873  subadd4  8201  mulsub  8358  mgmidmo  12791  tgcl  13567
  Copyright terms: Public domain W3C validator