MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anim123i Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3anim123i.1 . . 3 (𝜑𝜓)
213ad2ant1 1133 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1134 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1135 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1128 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff setvar class
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  7458  eloprabgaOLD  7459  le2tri3i  11243  fzmmmeqm  13428  elfz0fzfz0  13500  elfzmlbp  13506  elfzo1  13576  ssfzoulel  13620  flltdivnn0lt  13692  pfxeq  14538  swrdswrd  14547  swrdccat  14577  modmulconst  16124  nndvdslegcd  16339  ncoprmlnprm  16557  setsstruct2  17000  efmnd2hash  18658  symg2hash  19126  pmtrdifellem2  19212  unitgrp  20043  isdrngd  20161  bcthlem5  24638  lgsmulsqcoprm  26637  noetalem2  27036  colinearalg  27704  axcontlem8  27765  cplgr3v  28228  2wlkdlem3  28717  umgr2adedgwlk  28735  elwwlks2  28756  clwwlkinwwlk  28829  3wlkdlem5  28952  3wlkdlem6  28954  3wlkdlem7  28955  3wlkdlem8  28956  numclwwlk1lem2foalem  29140  chirredlem2  31178  rexdiv  31624  bnj944  33378  bnj969  33386  nnssi2  34859  nnssi3  34860  isdrngo2  36349  leatb  37686  paddasslem9  38223  paddasslem10  38224  dvhvaddass  39492  expgrowthi  42518  elsetpreimafveq  45484  nnsum4primesodd  45883  nnsum4primesoddALTV  45884  nn0mnd  46008  2zrngasgrp  46133  2zrngmsgrp  46140  mapprop  46317  lincvalpr  46394  refdivmptf  46523  refdivmptfv  46527  itsclc0yqsollem2  46744
  Copyright terms: Public domain W3C validator