Theorem an4s 672

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

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  an42s  673  anandis  690  anandirs  691  ax13  2409  nfeqf  2415  frminex  5630  trin2  6113  funprg  6579  funcnvqp  6589  fnun  6639  2elresin  6646  f1cof1  6776  f1oun  6830  f1oco  6834  fvreseq0  7023  f1mpt  7249  poxp  8112  soxp  8113  poseq  8142  wfr3g  8304  tfrlem7  8358  oeoe  8573  brecop  8796  pmss12g  8855  dif1ennnALT  9225  fiin  9370  tcmin  9696  frr3g  9716  harval2  9971  genpv  10972  genpdm  10975  genpnnp  10978  genpcd  10979  genpnmax  10980  addcmpblnr  11042  ltsrpr  11050  addclsr  11056  mulclsr  11057  addasssr  11061  mulasssr  11063  distrsr  11064  mulgt0sr  11078  addresr  11111  mulresr  11112  axaddf  11118  axmulf  11119  axaddass  11129  axmulass  11130  axdistr  11131  mulgt0  11275  mul4  11366  add4  11419  2addsub  11459  addsubeq4  11460  sub4  11491  muladd  11634  mulsub  11645  mulge0  11720  add20i  11745  mulge0i  11749  mulne0  11844  divmuldiv  11903  rec11i  11944  ltmul12a  12059  mulge0b  12073  zmulcl  12631  uz2mulcl  12938  qaddcl  12977  qmulcl  12979  qreccl  12981  rpaddcl  13028  xmulgt0  13297  xmulge0  13298  ixxin  13377  ge0addcl  13475  ge0xaddcl  13477  fzadd2  13575  serge0  14080  expge1  14123  sqrmo  15290  rexanuz  15385  amgm2  15409  bhmafibid1cn  15505  bhmafibid2cn  15506  mulcn2  15635  dvds2ln  16335  opoe  16409  omoe  16410  opeo  16411  omeo  16412  divalglem6  16444  divalglem8  16446  lcmcllem  16642  lcmgcd  16653  lcmdvds  16654  pc2dvds  16927  catpropd  17753  gimco  19326  efgrelexlemb  19808  psgnghm  21687  pf1ind  22472  tgcl  23083  innei  23239  iunconnlem  23541  txbas  23681  txss12  23719  txbasval  23720  tx1stc  23764  fbunfip  23983  tsmsxp  24269  blsscls2  24618  bddnghm  24840  qtopbaslem  24872  iimulcl  25053  icoopnst  25055  iocopnst  25056  iccpnfcnv  25060  mumullem2  27298  fsumvma  27331  lgslem3  27417  pntrsumbnd2  27685  mulsuniflem  28296  readdscl  28646  remulscllem2  28648  remulscl  28649  ajmoi  31115  hvadd4  31293  hvsub4  31294  shsel3  31572  shscli  31574  shscom  31576  chj4  31792  5oalem3  31913  5oalem5  31915  5oalem6  31916  hoadd4  32041  adjmo  32089  adjsym  32090  cnvadj  32149  leopmuli  32390  mdslmd1lem2  32583  chirredlem2  32648  chirredi  32651  cdjreui  32689  addltmulALT  32703  reofld  33573  xrge0iifcnv  34235  funtransport  36389  btwnconn1lem13  36457  btwnconn1lem14  36458  outsideofeu  36489  outsidele  36490  funray  36498  lineintmo  36515  bj-nnfan  37236  bj-nnfor  37238  icoreclin  37858  poimirlem27  38153  heicant  38161  itg2gt0cn  38181  bndss  38292  isdrngo3  38465  riscer  38494  intidl  38535  rimco  43144  unxpwdom3  43679  gbegt5  48382