ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim12i GIF version

Theorem anim12i 321
Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
Hypotheses
Ref Expression
anim12i.1 (𝜑𝜓)
anim12i.2 (𝜒𝜃)
Assertion
Ref Expression
anim12i ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem anim12i
StepHypRef Expression
1 anim12i.1 . 2 (𝜑𝜓)
2 anim12i.2 . 2 (𝜒𝜃)
3 id 19 . 2 ((𝜓𝜃) → (𝜓𝜃))
41, 2, 3syl2an 273 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  anim12ci  322  anim1i  323  anim2i  324  hban  1439  sbimi  1647  spsbbi  1725  2exeu  1992  cgsex2g  2590  cgsex4g  2591  spc2egv  2642  spc2gv  2643  sseq2  2967  unssin  3176  uneqin  3188  undif3ss  3198  prneimg  3545  ssunieq  3613  iuneq1  3670  iuneq2  3673  copsex2t  3982  soeq2  4053  tpexg  4179  eldifpw  4208  iunpw  4211  peano5  4321  opbrop  4419  xpsspw  4450  coeq1  4493  coeq2  4494  cnveq  4509  dmeq  4535  sotri  4720  elxp4  4808  elxp5  4809  funun  4944  funtp  4952  imain  4981  2elresin  5010  funssxp  5060  fssres  5066  f1co  5101  foun  5145  resdif  5148  f1oco  5149  fvun1  5239  fvreseq  5271  ftpg  5347  f1o2ndf1  5849  smores  5907  nnaord  6082  nnm00  6102  brecop  6196  eroveu  6197  ecopovtrn  6203  ecopovtrng  6206  th3qlem1  6208  th3q  6211  addcmpblnq  6465  mulcmpblnq  6466  mulclnq  6474  dmaddpq  6477  dmmulpq  6478  mulcanenq  6483  distrnqg  6485  ltdcnq  6495  ltexnqq  6506  enq0breq  6534  mulcmpblnq0  6542  mulcanenq0ec  6543  addnnnq0  6547  mulnnnq0  6548  mulclnq0  6550  nqpnq0nq  6551  nqnq0a  6552  nqnq0m  6553  distrnq0  6557  elinp  6572  genpml  6615  genpmu  6616  genprndl  6619  genprndu  6620  addnqprl  6627  addnqpru  6628  distrlem1prl  6680  distrlem1pru  6681  ltsopr  6694  cauappcvgprlemdisj  6749  caucvgprlemdisj  6772  caucvgprprlemdisj  6800  addcmpblnr  6824  addsrpr  6830  mulsrpr  6831  addclsr  6838  addasssrg  6841  0idsr  6852  1idsr  6853  00sr  6854  mulgt0sr  6862  axaddcl  6940  axmulcl  6942  axaddass  6946  axdistr  6948  cnegexlem3  7188  cnegex  7189  apirr  7596  recexaplem2  7633  zletric  8289  zlelttric  8290  qaddcl  8570  qmulcl  8572  qreccl  8576  iccss  8810  fzsubel  8923  elfz0add  8979  difelfznle  8993  2ffzeq  8998  fzonmapblen  9043  ubmelfzo  9056  ubmelm1fzo  9082  subfzo0  9097  qletric  9099  qlelttric  9100  adddivflid  9134  mulexp  9294  mulexpzap  9295  leexp1a  9309  rexanuz  9587  sqabsadd  9653  sqabssub  9654  abs2dif  9702  bj-indind  10056  peano5setOLD  10065
  Copyright terms: Public domain W3C validator