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  6488  ecopoveq  6629  enqdc  7359  addcmpblnq  7365  addpipqqslem  7367  addpipqqs  7368  addclnq  7373  addcomnqg  7379  distrnqg  7385  recexnq  7388  ltdcnq  7395  ltexnqq  7406  enq0enq  7429  enq0sym  7430  enq0breq  7434  addclnq0  7449  distrnq0  7457  mulclsr  7752  axmulass  7871  axdistr  7872  subadd4  8200  mulsub  8357  mgmidmo  12790  tgcl  13534
  Copyright terms: Public domain W3C validator