Theorem an4s 558

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 556	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 120	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

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:  an42s  559  anandis  562  anandirs  563  trin2  4866  fnun  5165  2elresin  5170  f1co  5276  f1oun  5321  f1oco  5324  f1mpt  5604  poxp  6059  tfrlem7  6144  brecop  6449  th3qlem1  6461  oviec  6465  pmss12g  6499  addcmpblnq  7076  mulcmpblnq  7077  mulpipqqs  7082  mulclnq  7085  mulcanenq  7094  distrnqg  7096  mulcmpblnq0  7153  mulcanenq0ec  7154  mulclnq0  7161  nqnq0a  7163  nqnq0m  7164  distrnq0  7168  genipv  7218  genpelvl  7221  genpelvu  7222  genpml  7226  genpmu  7227  genpcdl  7228  genpcuu  7229  genprndl  7230  genprndu  7231  distrlem1prl  7291  distrlem1pru  7292  ltsopr  7305  addcmpblnr  7435  ltsrprg  7443  addclsr  7449  mulclsr  7450  addasssrg  7452  addresr  7524  mulresr  7525  axaddass  7557  axmulass  7558  axdistr  7559  mulgt0  7710  mul4  7765  add4  7794  2addsub  7847  addsubeq4  7848  sub4  7878  muladd  8013  mulsub  8030  add20i  8121  mulge0i  8248  mulap0b  8277  divmuldivap  8333  ltmul12a  8476  zmulcl  8959  uz2mulcl  9252  qaddcl  9277  qmulcl  9279  qreccl  9284  rpaddcl  9314  ge0addcl  9605  ge0xaddcl  9607  expge1  10171  rexanuz  10600  amgm2  10730  iooinsup  10885  mulcn2  10920  dvds2ln  11321  opoe  11387  omoe  11388  opeo  11389  omeo  11390  lcmgcd  11552  lcmdvds  11553  tgcl  12015  innei  12114  txbas  12208  txss12  12216  txbasval  12217  blsscls2  12421  qtopbasss  12443  bj-indind  12715