Theorem jctild 527

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 514	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 397

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

This theorem is referenced by:  anc2li  557  equvini  2455  2reu1  3891  frpoinsg  6342  ordunidif  6411  isofrlem  7334  dfwe2  7758  orduniorsuc  7815  tfisg  7840  poxp  8111  fnse  8116  ssenen  9148  dffi3  9423  fpwwe2lem12  10634  zmulcl  12608  rpneg  13003  rexuz3  15292  cau3lem  15298  climrlim2  15488  o1rlimmul  15560  iseralt  15628  gcdzeq  16491  isprm3  16617  vdwnnlem2  16926  ablfaclem3  19952  epttop  22504  lmcnp  22800  dfconn2  22915  txcnp  23116  cmphaushmeo  23296  isfild  23354  cnpflf2  23496  flimfnfcls  23524  alexsubALT  23547  fgcfil  24780  bcthlem5  24837  ivthlem2  24961  ivthlem3  24962  dvfsumrlim  25540  plypf1  25718  noetalem1  27234  axeuclidlem  28210  usgr2wlkneq  29003  wwlksnredwwlkn0  29140  wwlksnextwrd  29141  clwlkclwwlklem2a1  29235  lnon0  30039  hstles  31472  mdsl1i  31562  atcveq0  31589  atcvat4i  31638  cdjreui  31673  issgon  33110  connpconn  34215  outsideofrflx  35088  isbasisrelowllem1  36225  isbasisrelowllem2  36226  poimirlem3  36480  poimirlem29  36506  poimir  36510  heicant  36512  equivtotbnd  36635  ismtybndlem  36663  cvrat4  38303  linepsubN  38612  pmapsub  38628  osumcllem4N  38819  pexmidlem1N  38830  dochexmidlem1  40320  cantnfresb  42060  harval3  42275  clcnvlem  42360  iccpartimp  46072  sbgoldbwt  46432  sbgoldbst  46433  elsetrecslem  47698