Theorem an4s 588

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

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:  an42s  589  anandis  592  anandirs  593  trin2  5012  fnun  5314  2elresin  5319  f1co  5425  f1oun  5473  f1oco  5476  f1mpt  5762  poxp  6223  tfrlem7  6308  brecop  6615  th3qlem1  6627  oviec  6631  pmss12g  6665  addcmpblnq  7341  mulcmpblnq  7342  mulpipqqs  7347  mulclnq  7350  mulcanenq  7359  distrnqg  7361  mulcmpblnq0  7418  mulcanenq0ec  7419  mulclnq0  7426  nqnq0a  7428  nqnq0m  7429  distrnq0  7433  genipv  7483  genpelvl  7486  genpelvu  7487  genpml  7491  genpmu  7492  genpcdl  7493  genpcuu  7494  genprndl  7495  genprndu  7496  distrlem1prl  7556  distrlem1pru  7557  ltsopr  7570  addcmpblnr  7713  ltsrprg  7721  addclsr  7727  mulclsr  7728  addasssrg  7730  addresr  7811  mulresr  7812  axaddass  7846  axmulass  7847  axdistr  7848  mulgt0  8006  mul4  8063  add4  8092  2addsub  8145  addsubeq4  8146  sub4  8176  muladd  8315  mulsub  8332  add20i  8423  mulge0i  8551  mulap0b  8585  divmuldivap  8642  ltmul12a  8790  zmulcl  9279  uz2mulcl  9581  qaddcl  9608  qmulcl  9610  qreccl  9615  rpaddcl  9648  ge0addcl  9952  ge0xaddcl  9954  expge1  10527  rexanuz  10965  amgm2  11095  iooinsup  11253  mulcn2  11288  dvds2ln  11799  opoe  11867  omoe  11868  opeo  11869  omeo  11870  lcmgcd  12045  lcmdvds  12046  pc2dvds  12296  tgcl  13135  innei  13234  txbas  13329  txss12  13337  txbasval  13338  blsscls2  13564  qtopbasss  13592  lgslem3  13974  bj-indind  14244