Theorem 3anim123i 1169

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 1151	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1152	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1153	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1146	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anim1i  1170  3anim2i  1171  3anim3i  1172  syl3an  1178  syl3anl  1442  eloprabga  7523  le2tri3i  11367  fzmmmeqm  13615  elfz0fzfz0  13691  elfzmlbp  13697  elfzo1  13771  ssfzoulel  13819  fvf1tp  13853  flltdivnn0lt  13897  hash7g  14554  pfxeq  14768  swrdswrd  14777  swrdccat  14807  modmulconst  16381  nndvdslegcd  16598  ncoprmlnprm  16822  setsstruct2  17269  efmnd2hash  19006  symg2hash  19522  pmtrdifellem2  19607  unitgrp  20527  isdrng3lem2  20918  isdrngd  20934  isdrngdOLD  20936  bcthlem5  25559  lgsmulsqcoprm  27582  noetalem2  27981  colinearalg  29370  axcontlem8  29431  cplgr3v  29898  2wlkdlem3  30398  umgr2adedgwlk  30416  elwwlks2  30440  clwwlkinwwlk  30513  3wlkdlem5  30646  3wlkdlem6  30648  3wlkdlem7  30649  3wlkdlem8  30650  numclwwlk1lem2foalem  30834  chirredlem2  32875  rexdiv  33374  bnj944  35450  bnj969  35458  wevonprcf1o  35713  nmulprop  36773  nnssi2  37077  nnssi3  37078  isdrngo2  38711  leatb  40168  paddasslem9  40704  paddasslem10  40705  dvhvaddass  41973  expgrowthi  45160  elsetpreimafveq  48300  nnsum4primesodd  48715  nnsum4primesoddALTV  48716  gpgusgralem  48975  nn0mnd  49097  2zrngasgrp  49164  2zrngmsgrp  49171  mapprop  49279  lincvalpr  49351  refdivmptf  49475  refdivmptfv  49479  itsclc0yqsollem2  49696