Theorem jca2 523

Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)

Hypotheses

Ref	Expression
jca2.1	⊢ (𝜑 → (𝜓 → 𝜒))
jca2.2	⊢ (𝜓 → 𝜃)

Assertion

Ref	Expression
jca2	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jca2

Step	Hyp	Ref	Expression
1		jca2.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jca2.2	. . 3 ⊢ (𝜓 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

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

This theorem is used by:  rr19.28v  3629  preddowncl  6337  ssimaex  6970  onfununi  8330  oaordex  8545  domtriord  9114  findcard3  9246  unfilem1  9268  inf0  9593  inf3lem3  9602  tcel  9715  fidomtri2  9992  alephval3  10106  zorn2lem6  10496  fodomb  10521  eqreznegel  12969  iserodd  16912  cshwsiun  17176  txcn  23812  ssfg  24058  fclsnei  24205  eldmgm  27215  fnrelpredd  35499  cvmlift2lem10  35817  axtco1from2  37019  bj-axreprepsep  37745  relcnveq3  39009  iss2  39026  elrelscnveq3  39309  jca3  39663  prjspreln0  43374  omabs2  44092  tfsconcatrn  44102  rfovcnvf1od  44763  mnuop3d  45014  ssclaxsep  45724