Theorem an4s 596

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

Hypothesis

Ref	Expression
an4s.1	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
an4s	⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Proof of Theorem an4s

Step	Hyp	Ref	Expression
1		an4 592	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 121	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an42s  597  anandis  600  anandirs  601  trin2  5179  fnun  5489  2elresin  5494  f1co  5610  f1oun  5659  f1oco  5662  f1mpt  5977  poxp  6468  tfrlem7  6588  brecop  6899  th3qlem1  6911  oviec  6915  pmss12g  6956  addcmpblnq  7735  mulcmpblnq  7736  mulpipqqs  7741  mulclnq  7744  mulcanenq  7753  distrnqg  7755  mulcmpblnq0  7812  mulcanenq0ec  7813  mulclnq0  7820  nqnq0a  7822  nqnq0m  7823  distrnq0  7827  genipv  7877  genpelvl  7880  genpelvu  7881  genpml  7885  genpmu  7886  genpcdl  7887  genpcuu  7888  genprndl  7889  genprndu  7890  distrlem1prl  7950  distrlem1pru  7951  ltsopr  7964  addcmpblnr  8107  ltsrprg  8115  addclsr  8121  mulclsr  8122  addasssrg  8124  addresr  8205  mulresr  8206  axaddass  8240  axmulass  8241  axdistr  8242  mulgt0  8401  mul4  8460  add4  8489  2addsub  8542  addsubeq4  8543  sub4  8573  muladd  8713  mulsub  8730  add20i  8822  mulge0i  8951  mulap0b  8986  divmuldivap  9045  ltmul12a  9193  zmulcl  9703  uz2mulcl  10018  qaddcl  10045  qmulcl  10047  qreccl  10052  rpaddcl  10089  ge0addcl  10394  ge0xaddcl  10396  expge1  11028  rexanuz  11770  amgm2  11901  iooinsup  12062  mulcn2  12097  dvds2ln  12610  opoe  12681  omoe  12682  opeo  12683  omeo  12684  lcmgcd  12875  lcmdvds  12876  pc2dvds  13132  tgcl  15256  innei  15355  txbas  15450  txss12  15458  txbasval  15459  blsscls2  15685  qtopbasss  15713  lgslem3  16287  bj-indind  17124