Theorem 3anim123i 1167

Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)

Hypotheses

Ref	Expression
3anim123i.1	⊢ (𝜑 → 𝜓)
3anim123i.2	⊢ (𝜒 → 𝜃)
3anim123i.3	⊢ (𝜏 → 𝜂)

Assertion

Ref	Expression
3anim123i	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Proof of Theorem 3anim123i

Step	Hyp	Ref	Expression
1		3anim123i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3ad2ant1 1149	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1150	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1151	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1144	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1101

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  df-3an 1103

This theorem is referenced by:  3anim1i  1168  3anim2i  1169  3anim3i  1170  syl3an  1176  syl3anl  1440  eloprabga  7520  le2tri3i  11340  fzmmmeqm  13585  elfz0fzfz0  13661  elfzmlbp  13667  elfzo1  13741  ssfzoulel  13789  fvf1tp  13822  flltdivnn0lt  13866  hash7g  14523  pfxeq  14733  swrdswrd  14742  swrdccat  14772  modmulconst  16346  nndvdslegcd  16563  ncoprmlnprm  16787  setsstruct2  17234  efmnd2hash  18953  symg2hash  19462  pmtrdifellem2  19547  unitgrp  20465  isdrngd  20847  isdrngdOLD  20849  bcthlem5  25456  lgsmulsqcoprm  27473  noetalem2  27872  colinearalg  29201  axcontlem8  29262  cplgr3v  29726  2wlkdlem3  30217  umgr2adedgwlk  30235  elwwlks2  30259  clwwlkinwwlk  30332  3wlkdlem5  30455  3wlkdlem6  30457  3wlkdlem7  30458  3wlkdlem8  30459  numclwwlk1lem2foalem  30643  chirredlem2  32684  rexdiv  33186  bnj944  35271  bnj969  35279  wevonprcf1o  35496  nmulprop  36581  nnssi2  36855  nnssi3  36856  isdrngo2  38497  leatb  39956  paddasslem9  40492  paddasslem10  40493  dvhvaddass  41761  expgrowthi  44935  elsetpreimafveq  48035  nnsum4primesodd  48450  nnsum4primesoddALTV  48451  gpgusgralem  48710  nn0mnd  48833  2zrngasgrp  48900  2zrngmsgrp  48907  mapprop  49011  lincvalpr  49083  refdivmptf  49207  refdivmptfv  49211  itsclc0yqsollem2  49428