Theorem 3anim123i 1151

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 1133	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1135	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1128	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anim1i  1152  3anim2i  1153  3anim3i  1154  syl3an  1160  syl3anl  1415  eloprabga  7515  eloprabgaOLD  7516  le2tri3i  11343  fzmmmeqm  13533  elfz0fzfz0  13605  elfzmlbp  13611  elfzo1  13681  ssfzoulel  13725  flltdivnn0lt  13797  pfxeq  14645  swrdswrd  14654  swrdccat  14684  modmulconst  16230  nndvdslegcd  16445  ncoprmlnprm  16663  setsstruct2  17106  efmnd2hash  18774  symg2hash  19258  pmtrdifellem2  19344  unitgrp  20196  isdrngd  20389  isdrngdOLD  20391  bcthlem5  24844  lgsmulsqcoprm  26843  noetalem2  27242  colinearalg  28165  axcontlem8  28226  cplgr3v  28689  2wlkdlem3  29178  umgr2adedgwlk  29196  elwwlks2  29217  clwwlkinwwlk  29290  3wlkdlem5  29413  3wlkdlem6  29415  3wlkdlem7  29416  3wlkdlem8  29417  numclwwlk1lem2foalem  29601  chirredlem2  31639  rexdiv  32087  bnj944  33944  bnj969  33952  nnssi2  35335  nnssi3  35336  isdrngo2  36821  leatb  38157  paddasslem9  38694  paddasslem10  38695  dvhvaddass  39963  expgrowthi  43082  elsetpreimafveq  46055  nnsum4primesodd  46454  nnsum4primesoddALTV  46455  nn0mnd  46579  2zrngasgrp  46828  2zrngmsgrp  46835  mapprop  47012  lincvalpr  47089  refdivmptf  47218  refdivmptfv  47222  itsclc0yqsollem2  47439