Theorem ancri 574

Description: Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
ancri.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ancri	⊢ (𝜑 → (𝜓 ∧ 𝜑))

Proof of Theorem ancri

Step	Hyp	Ref	Expression
1		ancri.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 22	. 2 ⊢ (𝜑 → 𝜑)
3	1, 2	jca 554	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  bamalip  2585  gencbvex  3236  eusv2nf  4824  issref  5468  trsuc  5769  fo00  6129  eqfnov2  6720  caovmo  6824  bropopvvv  7200  tz7.48lem  7481  tz7.48-1  7483  oewordri  7617  epfrs  8551  ordpipq  9708  ltexprlem4  9805  xrinfmsslem  12081  hashfzp1  13158  swrdccat3a  13431  dfgcd2  15187  catpropd  16290  idmhm  17265  symg2bas  17739  psgndiflemB  19865  pmatcollpw2lem  20501  icccvx  22657  uspgr1v1eop  26034  esumcst  29906  ddemeas  30080  bnj600  30697  bnj852  30699  dfpo2  31353  bj-csbsnlem  32545  nzss  37998  iotasbc  38102  wallispilem3  39591  nnsum3primes4  40965  idmgmhm  41076