Theorem 3anim123i 1149

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  3anim1i  1150  3anim2i  1151  3anim3i  1152  syl3an  1158  syl3anl  1413  eloprabga  7518  eloprabgaOLD  7519  le2tri3i  11348  fzmmmeqm  13538  elfz0fzfz0  13610  elfzmlbp  13616  elfzo1  13686  ssfzoulel  13730  flltdivnn0lt  13802  pfxeq  14650  swrdswrd  14659  swrdccat  14689  modmulconst  16235  nndvdslegcd  16450  ncoprmlnprm  16668  setsstruct2  17111  efmnd2hash  18811  symg2hash  19300  pmtrdifellem2  19386  unitgrp  20274  isdrngd  20533  isdrngdOLD  20535  bcthlem5  25076  lgsmulsqcoprm  27082  noetalem2  27481  colinearalg  28435  axcontlem8  28496  cplgr3v  28959  2wlkdlem3  29448  umgr2adedgwlk  29466  elwwlks2  29487  clwwlkinwwlk  29560  3wlkdlem5  29683  3wlkdlem6  29685  3wlkdlem7  29686  3wlkdlem8  29687  numclwwlk1lem2foalem  29871  chirredlem2  31911  rexdiv  32359  bnj944  34247  bnj969  34255  nnssi2  35643  nnssi3  35644  isdrngo2  37129  leatb  38465  paddasslem9  39002  paddasslem10  39003  dvhvaddass  40271  expgrowthi  43394  elsetpreimafveq  46363  nnsum4primesodd  46762  nnsum4primesoddALTV  46763  nn0mnd  46855  2zrngasgrp  46926  2zrngmsgrp  46933  mapprop  47110  lincvalpr  47186  refdivmptf  47315  refdivmptfv  47319  itsclc0yqsollem2  47536