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  6512  ecopoveq  6655  enqdc  7389  addcmpblnq  7395  addpipqqslem  7397  addpipqqs  7398  addclnq  7403  addcomnqg  7409  distrnqg  7415  recexnq  7418  ltdcnq  7425  ltexnqq  7436  enq0enq  7459  enq0sym  7460  enq0breq  7464  addclnq0  7479  distrnq0  7487  mulclsr  7782  axmulass  7901  axdistr  7902  subadd4  8230  mulsub  8387  mgmidmo  12845  tgcl  14016
  Copyright terms: Public domain W3C validator