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  6463  mulcmpblnq  6464  mulclnq  6472  dmaddpq  6475  dmmulpq  6476  mulcanenq  6481  distrnqg  6483  ltdcnq  6493  ltexnqq  6504  enq0breq  6532  mulcmpblnq0  6540  mulcanenq0ec  6541  addnnnq0  6545  mulnnnq0  6546  mulclnq0  6548  nqpnq0nq  6549  nqnq0a  6550  nqnq0m  6551  distrnq0  6555  elinp  6570  genpml  6613  genpmu  6614  genprndl  6617  genprndu  6618  addnqprl  6625  addnqpru  6626  distrlem1prl  6678  distrlem1pru  6679  ltsopr  6692  cauappcvgprlemdisj  6747  caucvgprlemdisj  6770  caucvgprprlemdisj  6798  addcmpblnr  6822  addsrpr  6828  mulsrpr  6829  addclsr  6836  addasssrg  6839  0idsr  6850  1idsr  6851  00sr  6852  mulgt0sr  6860  axaddcl  6938  axmulcl  6940  axaddass  6944  axdistr  6946  cnegexlem3  7186  cnegex  7187  apirr  7594  recexaplem2  7631  zletric  8287  zlelttric  8288  qaddcl  8568  qmulcl  8570  qreccl  8574  iccss  8808  fzsubel  8921  elfz0add  8977  difelfznle  8991  2ffzeq  8996  fzonmapblen  9041  ubmelfzo  9054  ubmelm1fzo  9080  subfzo0  9095  qletric  9097  qlelttric  9098  adddivflid  9132  mulexp  9268  mulexpzap  9269  leexp1a  9283  rexanuz  9561  sqabsadd  9627  sqabssub  9628  abs2dif  9676  bj-indind  10030  peano5setOLD  10039
  Copyright terms: Public domain W3C validator