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

Theorem 3anim123i 1152
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 1134 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1135 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1136 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1129 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3anim1i  1153  3anim2i  1154  3anim3i  1155  syl3an  1161  syl3anl  1416  eloprabga  7469  eloprabgaOLD  7470  le2tri3i  11292  fzmmmeqm  13481  elfz0fzfz0  13553  elfzmlbp  13559  elfzo1  13629  ssfzoulel  13673  flltdivnn0lt  13745  pfxeq  14591  swrdswrd  14600  swrdccat  14630  modmulconst  16177  nndvdslegcd  16392  ncoprmlnprm  16610  setsstruct2  17053  efmnd2hash  18711  symg2hash  19180  pmtrdifellem2  19266  unitgrp  20103  isdrngd  20228  isdrngdOLD  20230  bcthlem5  24708  lgsmulsqcoprm  26707  noetalem2  27106  colinearalg  27901  axcontlem8  27962  cplgr3v  28425  2wlkdlem3  28914  umgr2adedgwlk  28932  elwwlks2  28953  clwwlkinwwlk  29026  3wlkdlem5  29149  3wlkdlem6  29151  3wlkdlem7  29152  3wlkdlem8  29153  numclwwlk1lem2foalem  29337  chirredlem2  31375  rexdiv  31824  bnj944  33590  bnj969  33598  nnssi2  34956  nnssi3  34957  isdrngo2  36446  leatb  37783  paddasslem9  38320  paddasslem10  38321  dvhvaddass  39589  expgrowthi  42687  elsetpreimafveq  45663  nnsum4primesodd  46062  nnsum4primesoddALTV  46063  nn0mnd  46187  2zrngasgrp  46312  2zrngmsgrp  46319  mapprop  46496  lincvalpr  46573  refdivmptf  46702  refdivmptfv  46706  itsclc0yqsollem2  46923
  Copyright terms: Public domain W3C validator