Theorem 3expib 1123

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1120	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 412	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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  df-3an 1090

This theorem is referenced by:  3anidm12  1420  mob  3714  eqbrrdva  5870  fcoOLD  6743  f1oiso2  7349  frxp  8112  onfununi  8341  smoel2  8363  smoiso2  8369  3ecoptocl  8803  ssfi  9173  f1domfi  9184  rex2dom  9246  dffi2  9418  elfiun  9425  dif1card  10005  infxpenlem  10008  cfeq0  10251  cfsuc  10252  cfflb  10254  cfslb2n  10263  cofsmo  10264  domtriomlem  10437  axdc3lem4  10448  axdc4lem  10450  ttukey2g  10511  tskxpss  10767  grudomon  10812  elnpi  10983  dedekind  11377  nn0n0n1ge2b  12540  fzind  12660  suprzcl2  12922  icoshft  13450  fzen  13518  hashgt23el  14384  hashfundm  14402  hashbclem  14411  seqcoll  14425  relexpsucl  14978  relexpsucr  14979  relexpfld  14996  shftuz  15016  mulgcd  16490  algcvga  16516  lcmneg  16540  ressbas  17179  ressbasOLD  17180  resseqnbas  17186  resslemOLD  17187  ressress  17193  psss  18533  tsrlemax  18539  isnmgm  18565  gsummgmpropd  18600  issgrpd  18621  iscmnd  19662  ring1ne0  20111  unitmulclb  20195  isdrngd  20390  isdrngdOLD  20392  issrngd  20469  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  abvn0b  20920  isphld  21207  mpfaddcl  21668  mpfmulcl  21669  pf1addcl  21872  pf1mulcl  21873  fitop  22402  hausnei2  22857  ordtt1  22883  locfincmp  23030  basqtop  23215  filfi  23363  fgcl  23382  neifil  23384  filuni  23389  cnextcn  23571  prdsmet  23876  blssps  23930  blss  23931  metcnp3  24049  hlhil  24960  volsup2  25122  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  sinq12ge0  26018  bcmono  26780  iswlkg  28901  umgrwwlks2on  29242  clwlkclwwlkfo  29293  3cyclfrgrrn1  29569  grpodivf  29822  ipf  29997  shintcli  30613  spanuni  30828  adjadj  31220  unopadj2  31222  hmopadj  31223  hmopbdoptHIL  31272  resvsca  32475  resvlem  32476  resvlemOLD  32477  submateq  32820  esumcocn  33109  bnj1379  33872  bnj571  33948  bnj594  33954  bnj580  33955  bnj600  33961  bnj1189  34051  bnj1321  34069  bnj1384  34074  f1resrcmplf1dlem  34120  cplgredgex  34142  cusgr3cyclex  34158  loop1cycl  34159  umgr2cycllem  34162  umgr2cycl  34163  acycgr2v  34172  cusgracyclt3v  34178  climuzcnv  34687  fness  35282  bj-idreseq  36091  bj-imdiridlem  36114  neificl  36669  metf1o  36671  isismty  36717  ismtybndlem  36722  ablo4pnp  36796  divrngcl  36873  keridl  36948  prnc  36983  lsmsatcv  37928  llncvrlpln2  38476  lplncvrlvol2  38534  linepsubN  38671  pmapsub  38687  dalawlem10  38799  dalawlem13  38802  dalawlem14  38803  dalaw  38805  diaf11N  39968  dibf11N  40080  ismrcd1  41484  ismrcd2  41485  mzpincl  41520  mzpadd  41524  mzpmul  41525  pellfundge  41668  imasgim  41890  sqrtcval  42440  stoweidlem2  44766  stoweidlem17  44781  imaelsetpreimafv  46111  opnneir  47587  i0oii  47600  io1ii  47601