Theorem jca2 521

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 520	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  rr19.28v  3626  preddowncl  6314  ssimaex  6947  onfununi  8306  oaordex  8521  domtriord  9089  findcard3  9221  unfilem1  9243  fodomfibOLD  9268  inf0  9570  inf3lem3  9579  tcel  9692  fidomtri2  9946  alephval3  10060  zorn2lem6  10452  fodomb  10477  eqreznegel  12929  iserodd  16862  cshwsiun  17126  txcn  23674  ssfg  23920  fclsnei  24067  eldmgm  27074  fnrelpredd  35348  cvmlift2lem10  35623  axtco1from2  36796  bj-axreprepsep  37521  relcnveq3  38787  iss2  38804  elrelscnveq3  39087  jca3  39441  prjspreln0  43152  omabs2  43870  tfsconcatrn  43880  rfovcnvf1od  44541  mnuop3d  44808  ssclaxsep  45519