Theorem 3anim123i 1240

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 1075	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1076	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1077	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1235	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anim1i  1241  3anim2i  1242  3anim3i  1243  syl3an  1360  syl3anl  1369  spc3egv  3270  eloprabga  6645  le2tri3i  10046  fzmmmeqm  12245  elfz1b  12279  elfz0fzfz0  12313  elfzmlbp  12319  elfzo1  12385  ssfzoulel  12428  flltdivnn0lt  12496  swrdswrd  13312  swrdccatin2  13338  swrdccat  13344  modmulconst  14851  mulmoddvds  14889  nndvdslegcd  15065  ncoprmlnprm  15274  symg2hash  17640  pmtrdifellem2  17720  unitgrp  18490  isdrngd  18595  bcthlem5  22933  lgsmulsqcoprm  24868  colinearalg  25590  axcontlem8  25651  usgra2adedgwlk  26142  chirredlem2  28634  rexdiv  28965  bnj944  30262  bnj969  30270  nnssi2  31624  nnssi3  31625  isdrngo2  32927  leatb  33597  paddasslem9  34132  paddasslem10  34133  dvhvaddass  35404  expgrowthi  37554  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  cplgr3v  40657  21wlkdlem3  41134  umgr2adedgwlk  41152  elwwlks2  41170  31wlkdlem5  41330  31wlkdlem6  41332  31wlkdlem7  41333  31wlkdlem8  41334  2zrngasgrp  41730  2zrngmsgrp  41737  lincvalpr  42001  refdivmptf  42134  refdivmptfv  42138