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

Theorem an42s 557
 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 556 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 534 1 (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  nnmsucr  6263  ecopoveq  6401  enqdc  6974  addcmpblnq  6980  addpipqqslem  6982  addpipqqs  6983  addclnq  6988  addcomnqg  6994  distrnqg  7000  recexnq  7003  ltdcnq  7010  ltexnqq  7021  enq0enq  7044  enq0sym  7045  enq0breq  7049  addclnq0  7064  distrnq0  7072  mulclsr  7354  axmulass  7462  axdistr  7463  subadd4  7780  mulsub  7933  tgcl  11818
 Copyright terms: Public domain W3C validator